Changes between Version 43 and Version 44 of Language

Timestamp:

05/22/23 09:23:42 (3 years ago)

Author:

siegel

Comment:

--

Language

@@ -804 +804 @@
 There are clauses for preconditions, postconditions, and other concepts.
 These are used in various experimental extensions of CIVL.
-Here me describe the two clauses which are fully supported and in effect by the CIVL model checker.
-
-=== Specifying a guard: `enabled_when`
+Here we describe only the clauses which are fully supported and used by the core CIVL model checker.
+
+=== Specifying a guard: `executes_when`
 
 This clause has syntax
-  `enabled_when` ''expr'' `;`
+  `executes_when` ''expr'' `;`
 It may be used with an [#atomic_f atomic] or [#system system] function.
 This clause specifies a guard that applies whenever the function is called.
-The ''expr'' may use the formal parameters of the functions as well as any other variables that are in scope.
+The ''expr'' may use the formal parameters of the function as well as any other variables that are in scope.
 Whenever control in a process is at a call to the function, the call will be enabled only if the guard evaluates to ''true''.
-The actual arguments used in the call are substituted for the formal parameters in the guard expression.
-
-Note: if the actual arguments have side-effects, they are automatically refactored so that the side-effects occur once, before the call.
+To evaluate the guard, the actual arguments used in the call are substituted for the formal parameters in the guard expression.
+
+Note: if the actual arguments have side-effects, the code is automatically refactored so that the side-effects occur once, before the call.
 I.e., the call
   ''f''`(`''expr,,1,,''`,` ''expr,,2,,''`,` ...`)`
@@ -833 +833 @@
 === The `depends_on` clause #depends_on
 
-`\nothing`
-
-=== The `executes_when` clause #executes_when
+A depends_on clause has the form
+  `depends_on` ( `\nothing` | ''access-list'' ) `;`
+where ''access-list'' has the form
+  `\access` `(` ''expr'' ( `,` ''expr'' )* `)`
+Each expression in the access list should have a pointer type.
+
+The clause specifies the dependency relation for the system or atomic function.
+This dependency information is used by the model checker's partial order reduction algorithm to restrict the interleavings explored.
+
+The precise semantics: for a process that is at a state from which a call to the function is enabled:
+any transition from another process that does not access any object pointed to by an expression in the access list
+will be independent of the function call.
+
+(Two transitions are independent if, from any state in which both are enabled, neither can disable the other, and the two transitions commute,
+i.e., executing the fist and then the second results in the same state as executing the second and then the first.)
+
+This clause should be used with care: it is possible to specify a depends-on clause which is not sound, i.e.,
+the clause may declare that two transitions are independent when they are not.
+In this case, the model checker may skip some interleaving on which a violation occurs, and report that a program is correct when it is not.
+This mechanism is intended for use by expert library developers.
+
+