Changes between Version 24 and Version 25 of Language

Timestamp:

05/19/23 17:59:43 (3 years ago)

Author:

siegel

Comment:

--

Language

@@ -571 +571 @@
 in the sense that it is not necessary to explore all interleavings from the state where the local is enabled.
 
+==== Example
+
+The following illustrates the difference between local and atomic regions.
+{{{
+int x = 0;
+void thread(int tid) {
+  $atomic {
+    x = tid;
+  }
+}
+int main() {
+  $parfor (int i:1..2) thread(i);
+  $assert(x==2); // violated
+}
+}}}
+The program above spawns two threads, each of which writes to shared variable `x` in an atomic block.
+The program has two possible executions: in one, thread 1 writes first, then thread 2 writes; in the other, thread 2 writes first, then thread 1 writes.
+The assertion is violated on the second execution.
+Running `civl verify` on this code will report a violation.
+
+{{{
+int x = 0;
+void thread(int tid) {
+  $local_start();
+  x = tid;
+  $local_end();
+}
+int main() {
+  $parfor (int i:1..2) thread(i);
+  $assert(x==2); // valid
+}
+}}}
+In this program, the threads write to `x` within a local region.  This program has only one execution: first thread 1 executes the complete local region, then thread 2 executes the complete local region.  Running `civl verify` on this code yields "all properties hold".
+
+==== Use of `$yield` within a local region
+
 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.