Changes between Initial Version and Version 1 of Changes2023

Timestamp:

05/24/23 22:47:15 (3 years ago)

Author:

siegel

Comment:

--

Changes2023

@@ +1 @@
+
+Name Changes
+{{{
+$local_start  --> $begin_local
+$local_end    --> $end_local
+$pathCondition --> $print_path_condition
+$hidden --> $is_hidden
+$assume_push --> $push_assumption
+$assume_pop --> $pop_assumption
+$read_set_push --> $push_reads
+$write_set_push --> $push_writes
+$read_set_pop --> $pop_reads
+$write_set_pop --> $pop_writes
+$read_set_peek --> $peek_reads
+$write_set_peek --> $peek_writes
+$atomic_f --> ?
+$default_value --> $initialize
+}}}
+
+
+add doc for `$is_concrete_int` (`civlc.cvh`).
+
+change def of `$choose_int` to:
+
+{{{
+$atomic_f int $choose_int(int n) {
+  if ($is_concrete_int(n))
+    return $choose_int_concrete(n);
+  else {
+    int x=0;
+    for (; x<n-1; x++) {
+      $choose {
+        ;
+        break;
+      }
+    }
+    return x;
+  }
+}
+}}}
+
+
+Move functions from civlc.cvh to libraries...
+{{{
+is_derefable, hide, reveal, hidden: pointer.cvh
+elaborate_domain: domain.cvh
+}}}
+
+`#pragma CIVL` --> `#pragma civl`  (OK?)
+
+`\executes_when`: make it work for atomic_f functions?
+
+
+
+Some functions do not appear in any header:
+  `$scope_defined`
+  `$proc_defined`
+
+Note: `$proc_null` is defined in `PP2CivlcTokenCConverter.java`
+from the preprocessor, `$proc_null` is just an IDENTIFIER.
+This class converts identifiers to the proper token.
+
+We should probably replaced these with a single primitive: `$defined`.
+
+Language change: atomic/yield/depends:
+
+Get rid of begin/end local funtions.
+
+Change grammar to allow the following kinds of statements:
+{{{
+  $atomic stmt
+  $yield stmt
+  $depends_on (expr) stmt
+}}}
+
+Example:
+{{{
+$depends_on(expr) $atomic {
+  A;
+  $atomic {
+    B;
+    $yield {
+      C // this code is outside of atomic
+    }
+    $depends_on(expr) ...;
+  }
+}
+}}}
+
+translation:
+{{{
+  $atomic S --> begin_atomic; S end_atomic;
+  $yield S --> begin_yield; S end_yield;
+}}}
+
+semantics:
+state:
+{{{
+  atomicStack: stack of {0,1}. (1=begin_atomic, 0=begin_yield), initially empty
+}}}
+transitions:
+{{{
+  begin_atomic:
+    enabled when lock is free or I own it, and first statement after begin_atomic is enabled
+    if I don't own lock, obtain lock
+    if atomicStack.length >= max : error
+    atomicStack.push(1)
+  end_atomic:
+    assert !atomicStack.isEmpty() && atomicStack.top==1
+    atomicStack.pop()
+    if atomicStack.isEmpty() || atomicStack.top==0, release lock
+  begin_yield:
+    enabled when true;
+    if I own lock, release lock;
+    if atomicStack.length >= max: error
+    atomicStack.push(0);
+  end_yield:
+    enabled when atomicStack==01* => (lock.isFree && first stmt after yield is enabled);
+    assert !atomicStack.isEmpty && atomicStack.top==0 
+    atomicStack.pop()
+    if !atomicStack.isEmpty && atomicStack.top==1, obtain lock
+}}}
+
+Language change:
+
+  `$assuming`
+
+  `$track (rs,ws) stmt`
+
+  `$untrack stmt`
+