atomic.mzi

(* This module could be useful in a sequential setting. In a
   concurrent setting, though, it is superseded by the modules
   [locks] and [wref] in the standard library. *)

(* A type of duplicable references with arbitrary (hence, possibly
   non-duplicable) content. *)

abstract ref a : type
fact duplicable (ref a)

(* Allocation. *)

val newref : [a] (consumes a) -> ref a

(* An atomic swap operation. *)

(* The effect of [swap (r, x)] is to atomically write [x] to [r] and
   return the previous value of [r]. *)

val swap : [a] (ref a, consumes a) -> a

(* Sequential locks. *)

(* A sequential lock is a lock whose acquisition *fails* when the lock
   is already taken. Hence, the programmer should convince herself that
   the lock will never be taken twice at the same time (either by
   different threads, or by a single thread). *)

(* Sequential locks are meant to be used in a sequential setting. They
   provide protection against re-entrancy, and offer access to a hidden
   invariant state. *)

abstract lock (p : perm) : type
fact duplicable (lock p)

(* Creation. *)

val newlock     : [p : perm] (| consumes p) -> lock p

(* Acquisition. *)

val acquire     : [p : perm] lock p -> (| p)
val try_acquire : [p : perm] lock p -> rich_bool empty p

(* Release. *)

val release     : [p : perm] (lock p | consumes p) -> ()