Changes between Version 33 and Version 34 of Language


Ignore:
Timestamp:
05/20/23 20:30:36 (3 years ago)
Author:
siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • Language

    v33 v34  
    4343In particular, each `$domain(n)` is a subtype of `$domain`.
    4444There are expressions for specifying domain values.
    45 Certain statements use domains, such as the “CIVL-for” loop `$for`.
     45Certain statements use domains, such as the [#for domain iteration statement] `$for`.
    4646
    4747=== The range type `$range` #range-type
    … …  
    4949An object of this type represents an ordered set of integers.
    5050Ranges are typically used as a step in constructing domains.
    51 They can also be used in quantified expressions to specify the domain of a bound variable (see `$forall` and `$exists`).
     51They can also be used in quantified expressions to specify the domain of a bound variable (see [#boolean-expressions $forall and $exists]).
    5252
    5353== Type qualifiers #qualifiers
    … …  
    8989===  Abstract (uninterpreted) functions: `$abstract` #abstract
    9090
    91 An abstract function declares a function without a body.  An abstract function is declared using a standard function prototype with the function qualifier `$abstract`, e.g.,
    92 {{{
    93   $abstract int f(int x);
    94 }}}
    95 An abstract function must have a non-void return type and take at least one parameter.   An invocation of an abstract function is an expression and can be used anywhere an expression is allowed.  The interpretation is an "uninterpreted function".    A unique symbolic constant of function type will be created, corresponding to the abstract function, and invocations are represented as applications of the uninterpreted function to the arguments. 
     91An abstract function declares a function without a body.
     92An abstract function is declared using a standard function prototype with the function qualifier `$abstract`, e.g.,
     93{{{
     94$abstract int f(int x);
     95}}}
     96An abstract function must have a non-void return type and take at least one parameter.
     97An invocation of an abstract function is an expression and can be used anywhere an expression is allowed.
     98The interpretation is an "uninterpreted function".
     99A unique symbolic constant of function type will be created, corresponding to the abstract function, and invocations are represented
     100as applications of the uninterpreted function to the arguments. 
    96101
    97102=== Atomic functions: `$atomic_f` #atomic_f
    … …  
    103108}
    104109}}}
    105 A call to such a function executes as a single atomic step, i.e., without interleaving from other processes.   Hence, this is only relevant for concurrent programs.  Declaring a function to be atomic is almost equivalent to placing `$atomic{ ... }` around the function body.   The difference is that in the latter case, the call to the function and the execution of the body are executed in two atomic steps, i.e., after activation frame is pushed onto the call stack, another process could execute before the first process obtains the atomic lock and executes its body.   For an atomic function, the entire sequence of events happens in one atomic step.
     110A call to such a function executes as a single atomic step, i.e., without interleaving from other processes.
     111Hence, this is only relevant for concurrent programs.
     112Declaring a function to be atomic is almost equivalent to placing `$atomic{ ... }` around the function body.
     113The difference is that in the latter case, the call to the function and the execution of the body are executed in two atomic steps, i.e.,
     114after the activation frame is pushed onto the call stack, another process could execute before the first process obtains the atomic lock and executes its body.
     115For an atomic function, the entire sequence of events happens in one atomic step.
    106116
    107117An atomic function must have a definition; in particular, neither a system function nor an abstract function may be declared using `$atomic_f`.
    … …  
    109119=== System functions: `$system` #system
    110120
    111 A system function is one in which the definition of the function is not provided in CIVL-C code, but is implemented instead in a certain Java class.  A system function is declared by adding the function qualifier `$system` to a function prototype.  Invocation of a system function always takes place in a single atomic step.
    112 
    113 A system function may have a guard, which is specified in the function contract using a `$executes_when` clause.  Unless constrained by its contract or other qualifiers, a system function may modify the stay in an arbitrary way.
     121A system function is one in which the definition of the function is not provided in CIVL-C code, but is implemented instead in a certain Java class.
     122A system function is declared by adding the function qualifier `$system` to a function prototype.
     123Invocation of a system function always takes place in a single atomic step.
     124
     125A system function may have a guard, which is specified in the function contract using a `$executes_when` clause.
     126Unless constrained by its contract or other qualifiers, a system function may modify the stay in an arbitrary way.
    114127
    115128=== Pure functions: `$pure` #pure
    … …  
    122135}
    123136}}}
    124 This means that the function is a mathematical function of its arguments only.    I.e., an invocation of the function has no side-effects and the return value depends on the arguments only (if called twice with the same arguments, it will return the same value, regardless of any differences in the state).   The user is responsible for ensuring that a function declared pure actually is pure.    If this is not the case, the model checker may produce incorrect results.
     137This means that the function is a mathematical function of its arguments only.
     138I.e., an invocation of the function has no side-effects and the return value depends on the arguments only.
     139(If called twice with the same arguments, it will return the same value, regardless of any differences in the state).
     140The user is responsible for ensuring that a function declared pure actually is pure.
     141If this is not the case, the model checker may produce incorrect results.
    125142
    126143== Expressions #expressions
    … …  
    191208
    192209=== The null process reference: `$proc_null` #proc_null
    193 The null process constant.  Similar to the NULL pointer, this gives an object of `$proc` type a defined value, and can be used in `==` and `!=` expressions.
     210The null process constant.
     211Similar to the NULL pointer, this gives an object of `$proc` type a defined value, and can be used in `==` and `!=` expressions.
    194212It cannot be used as the argument to `$wait` or `$waitall`.
    195213
    … …  
    232250=== Scope relational expressions #scope-expressions
    233251
    234 Let `s1` and `s2` be expressions of type `$scope`. The following are all CIVL-C expressions of boolean type:
     252Let `s1` and `s2` be expressions of [#scope-type type $scope]. The following are all CIVL-C expressions of boolean type:
    235253
    236254* `s1 == s2` holds iff `s1` and `s2` refer to the same dynamic scope.
    … …  
    241259* `s1 >= s2` is equivalent to `s2 <= s1`.
    242260
    243 Each of these expressions is erroneous if `s1` or `s2` is undefined.  This error is reported by the model checker.
     261Each of these expressions is erroneous if `s1` or `s2` is undefined.
     262This error is reported by the model checker.
    244263
    245264=== This process: `$self` #self
    … …  
    286305Upon reaching the end of the atomic block, the process releases the atomic lock and exits the block.
    287306
    288 There is an exception to atomicity: if the process inside the atomic block executes a `$yield` statement, it releases the atomic lock.
     307There is an exception to atomicity: if the process inside the atomic block executes a [#yield $yield statement], it releases the atomic lock.
    289308This allows other processes to execute, and even obtain the lock.
    290309At any point at which the atomic lock is free and the first statement following the `$yield` is enabled, the original process may re-obtain
    … …  
    343362=== Domain iteration statement: `$for` #for
    344363
    345 A domain statement has the form
     364A domain iteration statement has the form
    346365
    347366  `$for` `(``int` ''i,,1,,''`,` ...`,` ''i,,n,,'' `:` ''dom''`)` ''S''
    348367
    349 where ''i,,1,,'', . . . , ''i,,n,,'' are ''n'' identifiers, ''dom'' is an expression of type `$domain(`''n''`)`, and ''S'' is a statement.
     368where ''i,,1,,'', . . . , ''i,,n,,'' are ''n'' identifiers, ''dom'' is an expression of [#domain-type type $domain(n)], and ''S'' is a statement.
    350369The identifiers declare ''n'' variables of integer type.
    351370Control iterates over the values of the domain, assigning the integer variables the components of the current tuple in the domain at the start of each iteration.
    … …  
    362381}}}
    363382
    364 There is a also a parallel version of this construct, `$parfor`.
     383There is a also a parallel version of this construct, [#parfor $parfor].
    365384
    366385=== Parallel for loop: `$parfor` #parfor
    … …  
    370389  `$parfor` `(``int` ''i,,1,,''`,` ...`,` ''i,,n,,'' `:` ''dom''`)` ''S''
    371390
    372 The syntax is exactly the same as that for the sequential domain iteration loop `$for`, only with `$parfor` replacing `$for`.
     391The syntax is exactly the same as that for the sequential [#for domain iteration statement $for], only with `$parfor` replacing `$for`.
    373392
    374393The semantics are as follows: when control reaches the loop, one process is spawned for each element of the domain.
    … …  
    414433$when (s>0) s--; t++;
    415434}}}
    416 To make the entire statement atomic, one must use an `$atomic` statement; see the following example.
     435To make the entire statement atomic, one must use an [#atomic $atomic statement]; see the following example.
    417436
    418437==== Example
    … …  
    464483$system void $assume(_Bool expr);
    465484}}}
    466 During verification, the given expression is assumed to hold. If this leads to a contradiction on some execution, that execution is simply ignored. It never reports a violation, it only restricts the set of possible executions that will be explored by the verification algorithm.
    467 Like an assertion call, an assume call can be used any place a statement is expected. In addition, an assume call can be used in file scope to place restrictions on the global variables of the programs. For example,
     485During verification, the given expression is assumed to hold. If this leads to a contradiction on some execution, that execution is simply ignored.
     486It never reports a violation, it only restricts the set of possible executions that will be explored by the verification algorithm.
     487Like an assertion call, an assume call can be used any place a statement is expected.
     488In addition, an assume call can be used in file scope to place restrictions on the global variables of the programs.
     489For example,
    468490{{{
    469491$input int B, N;
    … …  
    482504
    483505In the symbolic semantics, they behave as follows: each process maintains a stack of boolean symbolic expressions known as the temporary assumption stack.
    484 At any state, the ''effective path condition'' is the conjunction of the permanent path condition , and the conjunction,
     506At any state, the ''effective path condition'' is the conjunction of the permanent path condition, and the conjunction,
    485507over all processes ''p'',  of all entries in the temporary assumption stack of ''p''.
    486508A call to `$assume_push` pushes a new assumption onto the temporary assumption stack of the process making the call.
    … …  
    512534=== Explicit elaboration of a domain: `$elaborate_domain` #elaborate_domain
    513535
    514 Forces explicit enumeration of the elements of a finite domain.  Signature
     536Forces explicit enumeration of the elements of a finite [#domain-type domain].  Signature
    515537{{{
    516538$system void $elaborate_domain($domain d);
    … …  
    581603}}}
    582604
    583 CIVL-C provides primitives to constrain the interleaving semantics of a program.
    584 The program state has a single atomic lock, initially free.
    585 At any state, if there is a thread ''t'' that owns the atomic lock, only ''t'' is enabled.
    586 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,
    587 then among such threads, the thread with lowest ID is the only enabled thread; that thread executes `$local_start` and obtains the lock.
    588 When ''t'' invokes `$local_end`, ''t'' relinquishes the atomic lock.
    589 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,
     605These primitives constrain the interleaving semantics of a program, similar to [#atomic the atomic statement].
     606As with `$atomic`, `$local_start` obtains the atomic lock and/or increments the multiplicity;
     607$local_end` decrements the multiplicity and/or releases the atomic lock.
     608At any state, if there is a process ''t'' that owns the atomic lock, only ''t'' is enabled.
     609
     610The difference is as follows: when the atomic lock is free, if there is some process at a `$local_start` statement
     611and the first statement following `$local_start` is enabled,
     612then among such processes, the process with lowest PID is the only enabled process; that process executes `$local_start` and obtains the lock.
     613When ''t'' invokes `$local_end`, ''t'' decrements the atomic multiplicity, and if that multiplicity reaches 0, ''t'' relinquishes the atomic lock.
     614Intuitively, this specifies a block of code to be executed atomically by one process, and also declares that the block should be treated as a local statement,
    590615in the sense that it is not necessary to explore all interleavings from the state where the local is enabled.
    591616
    … …  
    605630}
    606631}}}
    607 The program above spawns two threads, each of which writes to shared variable `x` in an atomic block.
     632The program above spawns two "threads", each of which writes to shared variable `x` in an atomic block.
    608633The 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.
    609634The assertion is violated on the second execution.
    … …  
    622647}
    623648}}}
    624 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".
     649In this program, the threads write to `x` within a local region.
     650This program has only one execution: first thread 1 executes the complete local region, then thread 2 executes the complete local region.
     651Running `civl verify` on this code yields "all properties hold".
    625652
    626653==== Example
    … …  
    641668also has only one execution.
    642669Thread 1 will execute local block A and then release the atomic lock.
    643 But at that point, thread 1 will again be the thread of lowest PID at a `$local_start()` and therefore will be the only enabled thread.
     670But at that point, thread 1 will again be the thread of lowest PID at a `$local_start` and therefore will be the only enabled thread.
    644671It will execute local block B, and only then will thread 2 execute.
    645672The code above is equivalent to
    … …  
    663690
    664691Note that a thread waiting to return from a `$yield` has no special priority, even if that `$yield` is inside at local region.
    665 Only `$local_start` grants a thread a special priority.
     692Only [#local $local_start] grants a thread a special priority.
    666693
    667694=== Heap memory allocation: `$malloc` and `$free` #malloc-free
    … …  
    713740}}}
    714741
    715 The yield function is used inside an atomic or local region to release the atomic lock so that other processes may execute.
     742The yield function is used inside an [#atomic atomic] or [#local local] region to release the atomic lock so that other processes may execute.
    716743The yielding process retains its current atomic lock multiplicity, so that if and when it regains the atomic lock, it proceeds executing
    717744with the same multiplicity it had before the yield.
    … …  
    719746`$yield` must be enabled.
    720747This statement behaves as a guard for regaining the atomic lock, just as the first statement of an atomic block, or the first statement
    721 following `$local_start()`, acts as a guard for entering an atomic or local region.
     748following `$local_start`, acts as a guard for entering an atomic or local region.
    722749The yielding process competes with other processes to obtain the lock; it does not have any special priority.
    723 In particular, if the lock is available and there is a process at a `$local_start()` call (and the first statement following the call is enabled), one such a process is guaranteed to obtain the lock.
     750In particular, if the lock is available and there is a process at a `$local_start` call (and the first statement following the call is enabled), one such a process is guaranteed to obtain the lock.
    724751
    725752== Macros #macros