Changes between Version 17 and Version 18 of Fundamentals

Timestamp:

05/14/23 16:52:59 (3 years ago)

Author:

siegel

Comment:

--

Fundamentals

@@ -103 +103 @@
 === `$atomic_f`
 
+A function is declared atomic using the function qualifier `$atomic_f`, e.g.,
+{{{
+$atomic_f int f(int x) {
+  ...
+}
+}}}
+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.
+
+An atomic function must have a definition; in particular, neither a system function nor an abstract function may be declared using `$atomic_f`.
+
 === `$system`
 
+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.
+
+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.
+
 === `$pure`
+
+A system or atomic function may be declared to be `$pure`, e.g.,
+{{{
+$pure $system double sin(double x);
+$pure $atomic_f double mysin(double x) {
+  return  x - x*x*x/6.;
+}
+}}}
+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.
 
 == Types