(* Copyright (C) 1989, Digital Equipment Corporation           *)
(* All rights reserved.                                        *)
(* See the file COPYRIGHT for a full description.              *)

(* Last modified on Wed Jun  6 21:20:07 1990 by muller         *)

(* This implementation of the Wr, WrClass and UnsafeWr interfaces is an
alternative to the WrRep module, that works properly when used with a garbage
collector that moves objects. The drawback is that it is a bit slower.

The main difference is that the pointers are actually implemented as
indices in the buff array of the writer *)

UNSAFE MODULE WrMove EXPORTS Wr, WrClass, UnsafeWr;
IMPORT Thread, Convert, Text, TextF;
FROM Thread IMPORT Alerted;

REVEAL
  Private = Thread.Mutex BRANDED OBJECT
              next, stop := -1;
	    END;

(* Recall that a Wr.T was defined in WrClass to consist of the Private
fields followed by the buffer structure. The Private fields start with
a Thread.Mutex, which is as expected, since UnsafeWr revealed that
Wr.T is a subtype of Thread.Mutex.

The basic idea is that wr.next points at the character of wr.buff that
will be written by the next call to PutChar.  The fast path through
FastPutChar writes this character and advances wr.next, until wr.next
= wr.stop, at which point the code takes a slower path: *)


<*INLINE*> PROCEDURE FastPutChar(wr: T; ch: CHAR)
   RAISES {Failure, Alerted, Error} =
  (* wr is clean and locked. *)
  BEGIN
    IF wr.next # wr.stop THEN
      wr.buff[wr.next] := ch;
      INC(wr.next)
    ELSE
       SlowPutChar(wr, ch)
    END
END FastPutChar;
(* wr is clean and locked *) 


(* Notice that FastPutChar does not update wr.cur, and therefore does
not maintain the validity of wr.  This saves time, and the correct
value for wr.cur can be computed from wr.next whenever a valid state
is required.

We call a writer ``clean'' if it satisfies the invariant of
FastPutChar; we will derive the precise definition of this invariant
bit by bit.  First, since the fast path through FastPutChar implements
PutChar by storing into the buffer and not flushing afterwards, we
conclude that a clean writer wr must satisfy the following condition:

C1. If wr.next # wr.stop, then wr is buffered and ready, and 
	wr.next = wr.st + cur(wr) - wr.lo

Notice the use of cur(wr) instead of wr.cur, since the latter value
may be invalid.

A noteworthy consequence of C1 is that in a clean writer, wr.next =
-1 implies wr.stop = -1.  (If wr.next were -1 but wr.stop were not,
then C1 would imply that -1 was a index in an open array, which is nonsense.)
Because both fields default to -1, a newly-allocated writer will
satisfy C1.  The first call to FastPutChar on a new writer will take
the slow path, which can set up the pointers so that subsequent calls
will be fast.
   
Next, consider that when the fast path of FastPutChar fills the buffer
it must preserve C1; therefore it must make next = stop if it fills
the buffer.  Thus a clean writer wr must satisfy

C2. If wr.next # wr.stop, then
 	wr.stop = wr.st + wr.hi - wr.lo

The fast path through FastPutChar maintains C2, since it doesn't affect the
consequent, and it can only make the antecedent false.

Next, consider that it must be possible to make a clean writer valid,
for example, in order to call its methods.  We will do this by
updating the cur field.  It follows that the lagging cur field must be
the only violation of validity; that is, a clean writer wr satisfies

C3. All the validity conditions V1 through V4 defined in 
   WrClass hold for wr, except that the equation for
   wr.cur in V1 may fail.

Inspection shows that the fast path through FastPutChar maintains C3.

To make a clean writer valid we will compute the correct value for wr.cur from
wr.next using the equation in C1.  Unfortunately, C1 only requires that this
equation hold when wr.next # wr.stop, but we will often need to make a clean
writer valid when these pointers are equal; for example, when the buffer fills.
We therefore add a condition that says that the equation holds whenever wr.next
is not -1:

C4. If wr.next # -1, then 
	wr.next = wr.st + cur(wr) - wr.lo

The fast path through FastPutChar maintains C4, since it increments
both sides of the equality by one.

Finally, we must deal with the case wr.next = -1, which is the case
in a writer that is newly allocated by the runtime system.  Such a
writer will be valid, since it was given to us by a class
implementation, and we have not yet invalidated it by any calls to
FastPutChar.  Thus we conclude that a clean writer wr satisfies:

C5. If wr.next = -1, then wr is valid. 

The fast path through FastPutChar maintains C5, since it maintains the
stronger invariant wr.next # -1.

We define a writer to be clean if it satisfies C1--C5.

Conditions C3, C4, and C5 justify the following procedure for making 
a clean writer valid: *)


<*INLINE*> PROCEDURE MakeValid(wr: T) =
  (* wr is locked and clean. *) 
  BEGIN 
    IF wr.next # -1 THEN
      wr.cur := wr.lo + wr.next - wr.st
      END
  END MakeValid;
(* wr is locked, clean, and valid *) 


(* The reverse operation, MakeClean, sets the next and stop pointers
to produce a clean state.  It also returns a boolean indicating
whether the writer is ready.  Here is its spec: 

PROCEDURE MakeClean(wr: T): BOOLEAN

Assuming wr is valid and locked, set wr.next and wr.stop to produce a
valid clean state; furthermore if wr is ready and buffered, make
wr.next different from wr.stop.  Return TRUE if and only if the state
is ready.

MakeClean has two uses: to reset the next and stop pointers after a
class method has accessed the buffers, and to reset the pointers from
their initial NIL values the first time a writer is encountered by
this module.  (In the second case, MakeClean is being applied to a
writer that is already clean, in spite of its name.)

We will consider the implementation of MakeClean in a moment.  First
we will see how it is used in the code for SlowPutChar, which is a
long but straightforward case analysis, as is usual for the slow path
that takes care of all the cases that are ignored in the fast path: *)


PROCEDURE SlowPutChar(wr: T; ch: CHAR) RAISES {Failure, Alerted, Error} =
  (* wr is clean and locked; wr.next = wr.stop. *)
  BEGIN
    IF wr.closed THEN
      RAISE Error(Code.Closed)
    END;
    (* First goal is to make wr valid *)
    IF wr.next # -1 THEN
      MakeValid(wr)
    ELSE
      (* wr is already valid; but it might be newly allocated. *) 
      EVAL MakeClean(wr)
      (* wr is valid and clean, and if wr is ready
        and buffered, then wr.next is # -1  *) 
    END;
    (* wr is valid and clean *)  
    IF wr.cur = wr.hi THEN
      (* wr is valid, clean, and full *)    
      wr.seek(wr.cur);
      (* wr is valid and ready *)    
      IF NOT MakeClean(wr) THEN 
        RAISE Failure ("Seek method didn\'t make writer ready")
      END
      (* wr is valid, clean, and ready *)    
    END;
    (* wr is valid, clean, and ready *) 
    IF wr.next # wr.stop THEN
      wr.buff[wr.next] := ch;
      INC(wr.next)
    ELSE   
      (* wr is unbuffered *) 
      wr.buff[wr.st + wr.cur - wr.lo] := ch;
      INC(wr.cur);
      wr.flush()
    END
  END SlowPutChar;


(* Here is the implementation of MakeClean, which is short but tricky: *)

PROCEDURE MakeClean(wr: T): BOOLEAN =
  BEGIN
    IF (wr.lo <= wr.cur) AND (wr.cur < wr.hi)
        AND (wr.buff # NIL) AND (NOT wr.closed)
    THEN
      (* wr is ready *)
      wr.next := wr.st + wr.cur - wr.lo;
      wr.stop := wr.st + wr.hi - wr.lo;
      IF wr.stop < wr.next  THEN
          RAISE Failure ("Who\'s changing wr without the lock?")
      END;
      IF NOT wr.buffered THEN wr.stop := wr.next END;
      RETURN TRUE
    ELSE
      (* wr is not ready *)   
      wr.stop := -1;
      wr.next := -1;
      RETURN FALSE
    END
  END MakeClean;


(* The language requires that this procedure avoid unchecked runtime
errors even if a buggy class implementation is modifying the writer
without holding the lock.  The unsafe operations in this module are
the computations of wr.next and wr.stop, together with the increment
to wr.next.  The danger is that errors in the address arithmetic could
make wr.next point somewhere outside of wr.buff, causing PutChar to
spray characters randomly into memory. To prevent this, it suffices to
ensure that these two pointers both point into the array wr.buff^ (or
immediately after the array) and that they are in the proper order.
MakeClean guarantees this, since

1. In the computation of wr.next and wr.stop, the 
      subscripts into wr.buffP will be checked, and a runtime 
      error will occur if they are out of range, even if wr.st, 
      wr.cur, wr.hi, and wr.lo are changing concurrently.
2. The program checks that wr.next precedes wr.stop after
      computing them.

All of this may seem like paranoia, but the rule is that a module
exporting a safe interface must guarantee that no programing error by
a safe client of that interface can lead to an unchecked runtime
error.  Changing the buffer structure without locking the writer is a
possible programming error by a client of WrClass.  We therefore must
program WrRep in such a way that this error cannot lead to an
unchecked runtime error.  Otherwise we would have to add the word
``UNSAFE'' to the WrClass interface.

A client of UnsafeWr could call FastPutChar concurrently from two
threads, which could advance next past stop and clobber memory.  We
have no defense against this, which is why UnsafeWr is unsafe.

The remainder of the program is straightforward: *)


PROCEDURE Lock(wr: T) =
  BEGIN 
    Thread.Acquire(wr);
    MakeValid(wr)
  END Lock;

PROCEDURE Unlock(wr: T) =
  BEGIN
    EVAL MakeClean(wr);
    Thread.Release(wr)
  END Unlock;

<*INLINE*> PROCEDURE PutChar(wr: T; ch: CHAR) 
  RAISES {Failure, Alerted, Error} =
    (* wr must be unlocked. *)
  BEGIN
    LOCK wr DO FastPutChar(wr, ch) END
  END PutChar;


(* Although the designers of readers and writers think that the
procedures PutText, PutString, FastPutText, PutSub, FastPutString,
FastPutInt, FastPutReal, and FastPutLongReal are not very interesting,
it may be nice to implement them. So here they are. *)

PROCEDURE PutText (wr: T; t: TEXT) RAISES {Failure, Alerted, Error} =
  BEGIN
    LOCK wr DO
      FastPutText (wr, t); END;
  END PutText;

PROCEDURE FastPutText (wr: T; t: TEXT) RAISES {Failure, Alerted, Error} =
  VAR 
    start: CARDINAL := 0;
    length: CARDINAL := Text.Length (t);
    ch: CHAR;
  BEGIN
    WHILE (length > 0) DO
      WITH present = MIN (wr.stop - wr.next, length) DO
        FOR i := 0 TO present - 1 DO
          wr.buff[wr.next + i] := t[start + i]; END;
        INC (start, present);
        DEC (length, present);
        INC (wr.next, present);
	IF length > 0 THEN
          ch := Text.GetChar (t, start);
          INC (start);
          DEC (length);
          SlowPutChar (wr, ch); END; END; END;
  END FastPutText;

PROCEDURE PutString (wr: T; a: ARRAY OF CHAR)
   RAISES {Failure, Alerted, Error} =
  BEGIN
    LOCK wr DO
      FastPutString (wr, a); END;
  END PutString;

PROCEDURE FastPutString (wr: T; a: ARRAY OF CHAR)
   RAISES {Failure, Alerted, Error} =
  BEGIN
    FOR i := FIRST (a) TO LAST (a) DO
      FastPutChar (wr, a [i]) END;
  END FastPutString;

PROCEDURE FastPutInt (wr: T; n: INTEGER; base := 10)
   RAISES {Failure, Alerted, Error, Convert.Failed} =
VAR
  chars: ARRAY [0..BITSIZE(INTEGER) + 3] OF CHAR;
  size:  INTEGER;
BEGIN
  size := Convert.FromInt (chars, n, base);
  FOR i := 0 TO size - 1 DO
    FastPutChar (wr, chars[i]); END;
END FastPutInt;

PROCEDURE FastPutReal (wr: T; r: REAL; p: CARDINAL := 6;
                       s := Convert.Style.Mix)
   RAISES {Failure, Alerted, Error, Convert.Failed} =
VAR
  chars: ARRAY [0..100] OF CHAR;
  size:  INTEGER;
BEGIN
  size := Convert.FromFloat (chars, r, p, s);
  FOR i := 0 TO size - 1 DO
    FastPutChar (wr, chars[i]); END;
END FastPutReal;

PROCEDURE FastPutLongReal (wr: T; r: LONGREAL; p: CARDINAL := 6;
                           s := Convert.Style.Mix)
   RAISES {Failure, Alerted, Error, Convert.Failed} =
VAR
  chars: ARRAY [0..100] OF CHAR;
  size:  INTEGER;
BEGIN
  size := Convert.FromLongFloat (chars, r, p, s);
  FOR i := 0 TO size - 1 DO
    FastPutChar (wr, chars[i]); END;
  END FastPutLongReal;



   
PROCEDURE Seek(wr: T; n: CARDINAL) RAISES {Failure, Alerted} =
  BEGIN
    LOCK wr DO
      IF NOT wr.seekable THEN
        RAISE Failure ("Can\'t seek an unseekable writer")
      END;
      MakeValid(wr);
      TRY wr.seek(n) FINALLY EVAL MakeClean(wr) END
    END
  END Seek;

PROCEDURE GetIndex(wr: T): CARDINAL RAISES {} =
  BEGIN LOCK wr DO MakeValid(wr); RETURN wr.cur END END GetIndex;

PROCEDURE Length(wr: T): CARDINAL RAISES {Failure, Alerted} =
  BEGIN
    LOCK wr DO
      MakeValid(wr);
      TRY RETURN wr.length() FINALLY EVAL MakeClean(wr) END
    END
  END Length;

PROCEDURE Flush(wr: T) RAISES {Failure, Alerted} =
  BEGIN
    LOCK wr DO
      MakeValid(wr);
      TRY wr.flush() FINALLY EVAL MakeClean(wr) END
    END
  END Flush;

PROCEDURE Close(wr: T) RAISES {Failure, Alerted} =
  BEGIN
    LOCK wr DO
      IF NOT wr.closed THEN
        MakeValid(wr);
        TRY 
          wr.flush(); 
          wr.close() 
        FINALLY 
          wr.closed := TRUE;
          wr.next := wr.stop;
        END
      END
    END
  END Close;

PROCEDURE Seekable(wr: T): BOOLEAN RAISES {} =
  BEGIN
    LOCK wr DO RETURN wr.seekable END
  END Seekable;

PROCEDURE Closed(wr: T): BOOLEAN RAISES {} =
  BEGIN
    LOCK wr DO RETURN wr.closed END
  END Closed;

PROCEDURE Buffered(wr: T): BOOLEAN RAISES {} =
  BEGIN
    LOCK wr DO RETURN wr.buffered END
  END Buffered;

PROCEDURE CloseDefault(wr: T) RAISES {} =
  BEGIN wr.buff := NIL END CloseDefault;

PROCEDURE FlushDefault (<*UNUSED*> wr: T) RAISES {} =
  BEGIN END FlushDefault;

PROCEDURE LengthDefault(wr: T): CARDINAL RAISES {} =
  BEGIN RETURN wr.cur END LengthDefault;

BEGIN
END WrMove.


(* The reader may feel that our uncompromising pursuit of safety and 
efficiency has led to a design that is too complex.  The program would 
be much simpler if WrRep kept the writer valid at all times, 
and the cost would be only a few instructions per operation.  
The point is that our design allows a range of implementations 
of WrRep.  We have presented one that illustrates the issues 
that arise at the boundary between safe and unsafe code.  Substituting 
a simpler WrRep would not affect clients of Wr or of 
WrClass. *)