[M3devel] Proposed Atomic Word.T interfaces.

[Tony Hosking]

Thanks for the typo fixes.

On 20 Dec 2009, at 11:44, Rodney M. Bates wrote:

> To be legal on ADDRESS, either another parallel interface or a set of parallel
> procedures would be needed.  Or else, this interface would have to be known to
> the core language and allow predefined overloading, similar to builtin operators
> and functions.  The syntax could still be that of an interface.  I don't think
> any existing required interfaces do this now.

Perhaps better to make it a generic interface and instantiate for ADDRESS and Word.T:

GENERIC INTERFACE Atomic(Rep);

TYPE T = Rep.T;

TYPE
  Order = { Relaxed, Release, Acquire, AcquireRelease, Sequential };
  (* "Relaxed": The operation does not order memory.

     "Release": Performs a release operation on the affected memory locations,
     thus making regular memory writes visible to other threads through the
     variable to which it is applied.

     "Acquire": Performs an acquire operation on the affected memory
     locations, thus making regular memory writes in other threads released
     through the atomic variable to which it is applied, visible to the
     current thread.

     "AcquireRelease": The operation has both acquire and release semantics.

     "Sequential": The operation has both acquire and release semantics, and
     in addition, has sequentially-consistent operation ordering. *)

CONST IsLockFree = Rep.IsLockFree;
  (* True if the operations are lock-free, false otherwise. *)

PROCEDURE Store(VAR var: T; val: T; order := Order.Sequential);
  (* Atomically replace the value in "var" with "val".  Memory is affected as
     per "order".  The "order" shall be neither "Acquire" nor
     "AcquireRelease". *)

PROCEDURE Load(READONLY var: T; order := Order.Sequential): T;
  (* Atomically return the value in "var".  Memory is affected as per "order".
     The "order" shall be neither "Release" nor "AcquireRelease". *)

PROCEDURE Swap(VAR var: T; val: T; order := Order.Sequential): T;
  (* Atomically replace the value in "var" with "val". Returns the value of
     "var" immediately before the effects. Memory is affected as per order.
     This is a read-modify-write operation and synchronizes with any
     evaluation that reads the updated value. *)

PROCEDURE CompareSwap(VAR var, expected: T;
                      desired: T; order := Order.Sequential): BOOLEAN;
  (* Atomically, compares the value in "var" for equality with that in
     "expected", and if true, replaces the value in "var" with "desired", and
     if false, updates the value in "expected" with the value in "var".
     Returns the result of the comparison.  The "order" shall be neither
     "Release" nor "AcquireRelease".  This is a read-modify-write operation
     and synchronizes with any evaluation that reads the updated value.  The
     effect of the CompareSwap operation is:

     IF var = expected THEN var := desired ELSE expected := var;

     The CompareSwap operation may fail spuriously, that is return false while
     leaving the value in "expected" unchanged.  A consequence of spurious
     failure is that nearly all uses of CompareSwap will be in a loop:

     expected := Atomic.Load(current);
     DO
       desired := function(expected);
     WHILE NOT Atomic.CompareSwap(current, expected, desired);
  *)

PROCEDURE Fence(VAR var: T; order := Order.Sequential);
  (* Memory is affected as per "order".  Synchronizes with any operation on
     the same variable.  The "order" shall not be "Relaxed". *)

PROCEDURE FetchPlus (VAR var: T; incr: T; order := Sequential): T;
PROCEDURE FetchMinus(VAR var: T; decr: T; order := Sequential): T;
PROCEDURE FetchOr   (VAR var: T; mask: T; order := Sequential): T;
PROCEDURE FetchXOr  (VAR var: T; mask: T; order := Sequential): T;
PROCEDURE FetchAnd  (VAR var: T; mask: T; order := Sequential): T;
  (* Atomically replace the value in "var" with the result of the operation
     applied to the value in "var" and the given operand.  Memory is affected
     as per "order".  These operations are read-modify-write operations and
     synchronize with any evaluation that reads the updated value.  Returns
     the value of "var" immediately before the effects.

     For signed integral types, arithmetic is defined to use two's-complement
     representation. There are no undefined results.  For address types, the
     result may be an undefined address, but the operations otherwise have no
     undefined behavior. *)

END Atomic.