Changes between Version 20 and Version 21 of Libraries

Timestamp:

06/09/23 02:24:26 (3 years ago)

Author:

siegel

Comment:

Finish comm library and add mem library

Libraries

@@ -65 +65 @@
 * `$COMM_ANY_SOURCE`: a constant that can be used as the source argument in a dequeue operation to indicate that a message may be taken from any source
 * `$COMM_ANY_TAG`: a constant that can be used as the tag argument in a dequeue operation to indicate that a message with any tag may be selected
+* `$comm_null`: a constant representing the absence of `$comm`
 
 === Functions
@@ -98 +99 @@
   * Determines whether there exists a message with the given source and tag, and with destination the place of `comm`, in the gcomm associated to `comm`.   `source` may be `$COMM_ANY_SOURCE` and `tag` may be `$COMM_ANY_TAG`.
 * `$system $message $comm_seek($comm comm, int source, int tag)`
+  * Returns the oldest message in the gcomm associated to `comm` that matches `source` and `tag` without modifying gcomm. `source` may be `$COMM_ANY_SOURCE` and `tag` may be `$COMM_ANY_TAG`. If no such message found, returns a message with empty data and all meta-data being `-1`.
 * `$system $message $comm_dequeue($comm comm, int source, int tag)`
+  * Dequeues a message in a FIFO channel in the gcomm. The message should have its destination be the place of `comm`. The message will be dequeued from channel ''(i,j)'' in the gcomm, where ''i'' is the place of the source, and ''j'' is the place of the destination of the message.  A call to this function will not return until a matching message can be dequeued.
 * `$system $state_f _Bool $comm_empty_in($comm )`
+  * deprecated
 * `$system $state_f _Bool $comm_empty_out($comm )`
+  * deprecated
 
 
@@ -122 +127 @@
 Uses: (nothing).
 
+The `mem` library provides functions to manipulate objects of the CIVL-C built-in type---`$mem`.  A `$mem` object represents a set of memory locations.
+
+=== Functions
+
+* `$system void $write_set_push()`
+  * Pushes a new entry (i.e. an empty `$mem`) onto the write stack of the calling process.  Each process maintains a write stack. A write to a memory location will cause the memory location being added to the top entry of the write stack, if the stack is non-empty.
+* `$system $mem $write_set_pop()`
+  * Pops and returns the top entry of the write stack of the calling process.
+* `$state_f $system $mem $write_set_peek()`
+  * Returns the top entry of the write stack of the calling process.
+* `$system void $read_set_push()`
+  * Pushes a new entry (i.e. an empty `$mem`) onto the read stack of the calling process.  Each process maintains a read stack. Reading a memory location will cause the memory location being added to the top entry of the read stack, if the stack is non-empty.
+* `$system $mem $read_set_pop()`
+  * Pops and returns the top entry of the read stack of the calling process.
+* `$state_f $system $mem $read_set_peek()`
+  * Returns the top entry of the read stack of the calling process.
+* `$atomic_f $system $mem $mem_empty()`
+  * Creates a new empty `$mem` object.
+* `$atomic_f $system _Bool $mem_equals($mem m0, $mem m1)`
+  * Returns true iff `m0` and `m1` are the identical set of memory locations.
+* `$atomic_f $system _Bool $mem_contains($mem super, $mem sub)`
+  * Returns true iff `super` is a super-set of `sub`.
+* `$atomic_f $system _Bool $mem_no_intersect($mem m0, $mem m1, $mem *out0, $mem *out1)`
+  * Returns true iff `m0` and `m1` are two disjoint sets. If `m0` and `m1` overlap, `out0` and `out1` will be assigned two overlapping memory location sets, which are as small as the function can figure out from `m0` and `m1`, respectively.
+* `$atomic_f $system $mem $mem_union($mem mem0, $mem mem1)`
+  * Returns the union of the two sets of memory locations `mem0` and `mem1`.
+* `$atomic_f $system $mem $mem_union_widening($mem, $mem)`
+  * Similar to the `$mem_union` function but may return an over-approximated super-set of the union set.  The over-approximation is done by the model checker in order to make state space finite.
+* `$atomic_f $system void $mem_havoc($mem m)`
+  * Assigns arbitrary values to memory locations in `m`
+* `$atomic_f $system $mem $mem_unary_widening($mem m)`
+  * Returns an over-approximated super-set of `m`. The over-approximation is done by the model checker in order to make state space finite.
+* `$atomic_f $system void $mem_assign_from($state s, $mem m)`
+  * deprecated
 
 == op #op