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