Changes between Version 22 and Version 23 of Language

Timestamp:

05/19/23 17:42:22 (3 years ago)

Author:

siegel

Comment:

--

Language

@@ -555 +555 @@
 If `p` is undefined or `$proc_null`, returns 0.
 
-=== Modifying the dependence relation: `$local_start` and `$local_end`
-
+=== Specifying local regions: `$local_start` and `$local_end`
+
+CIVL-C provides primitives to constrain the interleaving semantics of a program.
+The program state has a single atomic lock, initially free. 
+At any state, if there is a thread ''t'' that owns the atomic lock, only ''t'' is enabled.
+When the atomic lock is free, if there is some thread at a `$local_start` statement, and the first statement following `$local_start` is enabled,
+then among such threads, the thread with lowest ID is the only enabled thread; that thread executes `$local_start` and obtains the lock.
+When ''t'' invokes `$local_end`, ''t'' relinquishes the atomic lock.
+Intuitively, this specifies a block of code to be executed atomically by one thread, and also declares that the block should be treated as a local statement,
+in the sense that it is not necessary to explore all interleavings from the state where the local is enabled.
+
+Local blocks can also be broken up at specified points using function `$yield`.
+If ''t'' owns the atomic lock and calls `$yield`, then ''t'' relinquishes the lock and does not immediately return from the call.
+When the atomic lock is free, there is no thread at a `$local_start`, a thread ''t'' is in a `$yield`, and the first statement following the `$yield` is enabled,
+then ''t'' may return from the `$yield` call and re-obtain the atomic lock.
 
 === Heap memory allocation: `$malloc` and `$free`