A Specification of Syntax and Semantics of RGITL in Higher-Order Logic

Syntax and semantics of the logic are documented in [TIME11]. More details are given in our journal article [AMAI14] (draft available here).

As a general convention, all the definitions of syntax and semantics of the specifications use leading underscores, to differentiate them from the implemented logic.

The overview over the specification structure shows, that it is quite big, and contains lots of definitions. In general, the specification is a deep embedding, i.e. syntax and semantics are specified separately.

The following is a bottom-up explanation. If you are just interested in the toplevel theorems, the rules for symbolic execution are proved here (for the chop operator) and here (for interleaving). The three fairness rules of [AMAI14] are proved here, here and here. The proof of monontonicity of procedure declarations is here, together with a proof of the unfolding axiom.

If you are interested in applications of RGITL, then browse to the following sites: the derivation of Theorem 6 from the paper (RG Reasoning), and the derivation of Theorem 7 (decomposition of lock-freedom) can be found on this page. For details on applications of RGITL on concrete algorithms refer this page.

Basic definitions of the Syntax

• The specification starts with a definition of types (KIV-type Ty). To differentiate between the sorts and types of KIV's specification language, and the elements of sort "Ty" specified for RGITL, we call the former KIV-types and KIV-sorts in the following. Ty is therefore a KIV-sort. KIV-type Ty contains sorts (among them the predefined sorts _bool and _nat), (unary) function types, pair types and reference types. Reference types are not (yet) used. As a minor difference to [TIME11], the specification uses unary functions and currying instead of n-ary functions, since the axioms are a bit easier this way.
• RGITL assumes unspecified sets of operations (KIV-type OP), flexible (KIV-type X) and static (KIV-type V) variables. Each of them has a type. The operations include predefined boolean operations (written with two underscores, to allow more convenient infix functions on expressions with one underscore later on).
• Procedures (KIV-type Proc) are defined.

Basic definitions of the Semantics (Algebras)

• The carrier sets of the underlying algebra are specified as one big universe (KIV-type U), that is their disjoint union.
  • The type of an element of the universe determines, to which carrier set it belongs.
  • If the type of an element u is ty1 _× ty2, then u.1 and u.2 select the two components of the pair, i.e. elements of U with types ty1 and ty2. If the type of u is not a pair type, then u.1 and u.2 are left unspecified.
  • If the type of u is a function type ty1 _→ ty2, and u0 has type ty1, then u[u0] applies this function to u0 (the apply operation . [ . ] has KIV-type U × U → U), yielding a result of type ty2. Again, if u does not have a function type, or if the type of u0 is different from ty2, u[u0] is not specified (i.e. yields an arbitrary element of U). .
  • The universe contains an embedding of the KIV-types of booleans and natural numbers . By convention, all embeddings of a smaller type into a bigger one are written with (overloaded) quine quotes.
  • The specification defines an embedding for pairs as function from U x U to U. The result has the pair type of the types of the two inputs.
  • The specification defines an embedding for functions (U → U) to U. Since the result is not uniquely determined, and cannot be guaranteed to be well-typed, the embedding is done with a function ftoU(f,ty1,ty2), that is applied to a function f with KIV-type U → U, and two types ty1, ty2. ftoU gives an element of U with type ty1 _→ ty2. The result is specified only, when f(u) is of type ty2 for every input u of type ty1, as specified by predicate wtf(f,ty1,ty2) (otherwise it is an arbitrary element of U with type ty1 _→ ty2). In this case using the apply operation is defined for elements u of type ty1, and ftoU(f,ty1,ty2)[u] yields f(u). If wtf does not hold, ftoU returns an arbitrary element of type ty1 _→ ty2.
• The semantics of an operations op 〚op〛 is an element of U of the same type as the type of the operation. The type and semantics of boolean operations is fixed in this specification.
• Procedures are given a (loose) Semantics.

Intervals

• The main constructor is mkI(flextrace, flextrace0, statstate, blocktrace, n∞). Its arguments are:
  • argument n∞ (a natural number or infinity ∞) determines the length of the interval (selected as # I for an arbitrary interval I)
  • a mapping statstate: V → U that determines the values of static variables (selected as I[v]).
  • a mapping flexstate : nat → X → U. flexstate(n)(x) is the value of variable x in the nth state of the interval (selected as I[n](x)).
  • a mapping flexstate0 : nat → X → U. flexstate0(n)(x) is the value of variable x in the nth primed state of the interval (selected as I[n]'(x))
  • a mapping blocktrace: nat → bool. blocktrace(n) determines whether the nth system step of the interval is blocked (selected as I[n]b)
• The constructor gives a defined interval only, when the arguments are well-typed (predicate wt). Otherwise, it yields an arbitrary interval. Predicate wt checks, that the type of static and flexible variables is the same as the type of the value they are mapped to. Also if the nth step is blocked, then flextrace(n) and flextrace0(n) must be identical. Note, that the values of flextrace(n), flextrace0(n) and blocktrace(n) are ignored for all n beyond the length of the interval.
• The specification defines various auxiliary functions: "I to n" and "I from n" are the intervals until system state n, resp. from system state n (written with subscripts as I_[0..n] and I_[n..] in [TIME11, AMAI14]). Both are defined for n ≤ # I.
• I[x] is the value sequence for variable x in interval I.
• predicate I1 =0 I2 asserts, that I1 and I2 have the same first state (flexible as well as static variables). I1 =s I2 asserts, that the static variables of I1 and I2 have the same values.
• consI adds a new (system and environment) step in front of an interval, tlI cuts away the leading step. appI(I1,n,I2) appends I2 at the end of the first n steps of I1. The operation is defined, if n ≤ # I1 and I1 =s I2. The operation ignores all states of I1 starting with state I1[n]. (so: appI(I1,n,I2) from n = I2, and: if I1[n] = I0[0], then appI(I1,n,I2) to n = I1).
• I[v,u] modifies the value of static variable v to be u (defined, when type(v) = type(u)).
• Given two functions uf,uf : X → U, then I[x,uf,uf0] modifies the value of x in I[n] to be uf(n), and in I[n]' to be uf0(n). The modification is defined, when wtx(I,x,uf,uf0) holds.

Interleaving of Intervals

• Specification interleaving defines interleaving of intervals.
  • "(I1 ∥sc I2)(I,sc)" is written "(I,sc) ∈ (I1 ⊕ I2)" in [TIME11, AMAI14].
  • The schedule sc is a sequence (formally the KIV-type of streams is used) of booleans. "true" means "left interval is scheduled", "false" means "right interval is scheduled". In [TIME11, AMAI14] values "1" and "2" are used, to give more intuition.
  • "(I1 ∥sc I2)(I,sc)" is defined to hold, when two sequences of natural numbers nσ1, nσ2 exist with "(I1 ∥esc I2)(I,sc,nσ1, nσ2)". The latter notation is written "(I,sc,l, r) ∈ (I1 ⊕ I2)" in [AMAI14] using letters l, r instead of nσ1, nσ2. The wo sequences fix, that "I1 from nσ1(k)" and "I2 from nσ2(k)" are interleaved to determine the kth step of I. The auxiliary predicate "∥1" is used to interleave a single step.
  • "(I1 ∥isc I2)(I,sc, nσ1, nσ2, sc1, sc2)" is an alternative definition of scheduled interleaving with inverse mappings. For n1 < # nσ1, I1[n1] is mapped to I[nσ1[n1]], and: if sc1[n1] is true, then I1[n1]' is mapped to I[nσ1[n1]]'.
  • The two definitions are proven equivalent. The proof is rather complex, and the specification contains some auxiliary functions and predicates that are needed for the two implications of this proof.
• Specification ilv-mod proves two important results about interleaving vs. modifying values of variables. The first theorem shows that modifying some variables (but leaving length and blocking information unchanged) of the result of interleaving can be propagated to the intervals that were interleaved. The second theorem shows the reverse direction. Both results can be specialized to specific modifications. They are such that only the variables modified in the changed interval are modified in the other intervals too. The special case of modifying just one flexible variable is proved here and here.

Expressions

• Expressions (KIV-type E) are defined as a free datatype. Small deviations from [TIME11, AMAI14] are
  • Notation cannot be "free mixfix". E.g. a universal quantifier is written "_∀(x,e)" instead of "∀ x. e". The basic operator of labelled left interleaving is written "_<||(L1,e1,L2,e2)" instead of "L1: e1 <∥ L2: e2". Formulas are not written as "ϕ", but as "e" (and "e" is constrained to have type _bool).
  • Since flexible and static variables are of a different type, there is a universal quantifier for each of them.
  • We use built-in pair expressions with constructor e1 _× e2, and selectors .1 and .2.
  • An additional prefix-Operator (see [FAC11]) is defined, that is needed for induction over general safety formulas.
  • Procedure calls have one value and one reference parameter only, to avoid constraints about duplicate-freeness. This is no severe restriction, since a parameter with tuple type can replace several parameters.
• Well-typed expressions should satisfy predicate wt to have a meaningful type and semantics.
• The semantics of expressions 〚e〛(I) follows the definitions of [TIME11, AMAI14]. Validity over an interval (I ⊧ e) and general validity (_⊧ e) for boolean expressions (= formulas) is defined here.
• A number of derived expressions are defined, and lemmas about their semantics are proved.
• All variables, and the free variables of an expression are defined here.
• Specification coincidence contains a proof of the coincidence lemma for RGITL. Predicate =xv(I1,xl,vl,I2) asserts, that I1 and I2 have the same length, and that their states agree on the values for the variables from lists xl of flexible and vl of static variables.
• Various subsets of expressions are defined:
  • The semantics of State expressions (predicate stateexpr?) depends on the first state of an interval only. They can therefore be given a semantics 〚e〛(s) based on one state s (of KIV-type S). (A state maps both flexible and static variables to values). The state semantics is equivalent to the normal semantics using state I[0]s as defined in this specification. Formulas with path quantifiers are included in predicate stateexpr?, as they indeed depend on the first state of an interval. However they should not be used in the tests and assignments of regular programs, so a second predicate pstateexpr? defines state expressions without path quantifiers (this predicate corresponds to the definition of state expressions in [AMAI14]).
  • Step expressions depend on the first (system and environment) step (proven as two theorems here and here).
  • The semantics of Static expressions depends on the values of static variables only, as proven here.
• Specification modvl-modxl defines quantification over a vector of variables as an abbreviation. It also contains definitions and theorems about modifying the values of a list of static and flexible variables in an interval I.

Programs

• Programs (KIV-type P) are the same as in [TIME11, AMAI14], except that nondeterministic or is used as an additional primitive. Notationally, [e]PL allows to use an arbitrary expression of type bool (using any temporal operators) as a program. Again mixfix notation (e.g. "if e then p1 else p2") is replaced with normal function application ("_if(e,p1,p2)" in the example). Well-typed programs satisfy predicate wt.
• The semantics of programs is defined as a shallow embedding: "{xl,p}" corresponds to "[p]_xl" (with xl as a subscript) in [TIME11, AMAI14].

Renaming, Substitutions and Symbolic Execution

• Specification repl-Expr defines functions "replv" and "replx" that renames a (static resp. flexible) variable to a new one (including bound renaming). The corresponding two substitution lemmas are proved here and here. Auxiliary specification norm-allpath contains a proof that an allpath quantifier can be normalized, such that its body has no free flexible variables, that is crucial for the definition of replacing variables in path quantifiers.
• The specification of Step expressions defines a function redlb(e,bv,bv0) that reduces a step expression based on information on whether this is the last state (then bv = true), and whether the first step is blocked (then bv0 = true). It replaces expressions last and blocked with true/false as appropriate, and replaces primed variables with unprimed ones, when bv = false, bv0 = true. For this case it is proved that the resulting expression depends on the values of its free variables in state I[0] and I[1] only (I[0]b and I'[0] can be modified). This result is needed for the correctness of symbolic execution rules for interleaving.
• The rules for symbolic execution are proved in two toplevel specifications: symbolicexec-chop proves the rules for compounds (chop operator) and symbolicexec-ilv proves the rules for interleaving (the rules for weak fair and unfair interleaving are the same) as theorems (the names are (nf)ilvl(b)- exx/exv/dis/stp/blk/lst). The proofs make use of a definition of substitutions as given in apply-stepsubst, that replaces x with e0, x' with e1, and x'' with e2. Variable ssubst is a list of quadruples (x,e0,e1,e2) of type ssub. Instances of this generic substitution scheme are used in the symbolic execution rules, in particular many of them replace x'' with a new static variable (called u in [AMAI14]). A substitution lemma, that shows, that applying such a substitutions on step expressions is equivalent to modifying the semantics of x by he values of e0,e1,e2 in the interval (as defined by operator @I), is proved.
• Specification apply-nsubst defines the general substitution scheme 𝒩 of [AMAI14] as an operator "@(e,nsubst,v)" defined for expressions, which are in step form (defined as predicate stepform?). The substitution replaces flexible variables x and x' with new static variables x_0 and x_1, x'' with x, step with true, and blocked with a boolean static variable v. Argument "nsubst" is a list of triples (x,x_0,x_1) of type nsub that are used for this purpose. Operator "@I(I,nsubst,v) is its semantic equivalent, that removes the first step of the interval, and maps the new static variables x_0, x_1 to the old values x had in I(0) and I'(0) and v to I(0)_b. The main theorem over the specification proves that the substitution is indeed equivalence preserving.
• Specification redlast contains a function redlast(e), which reduces every expression e to an equivalent state expression under the assumption "last" of an empty interval, corresponding to ℒ in [AMAI14]. Again, the main theorem of this specification shows that redlast(e) is indeed equivalent to e.

Fairness

• Specification fairness contains proofs for several fairness rules for (both weak fair and unfair) interleaving, including the three fairness rules given in [AMAI14]: here is the rule for fair interleaving, and here the one for non-fair interleaving. The extra rule that introduces a counter is proved here.

Procedure Declarations

• Specification procdecl-PD defines the type PD of procedure declarations, which is a tuple consisting of the procedure name, a formal value and reference parameter, and the body (several parameters could be imitated using a tuple).
• Using an extended semantics of expressions, that is parameterized with the meaning of procedures, it is possible to prove, that the semantics of a regular program is monotonic in the semantics of the procedures it calls.
• Therefore, according to Knaster-Tarski's fixpoint theorem, (which states that monontone functions have a least fixpoint; the theorem is given for sets, i.e. boolean functions), the semantics of a given list "thepdl" of procedure declarations (where bodys are regular programs) can be defined as a least fixpoint.
• Finally, the unfolding axiom can be proved, based on this definition.

Miscellaneous

• predicate safe? semantically characterizes safety formulas. These are valid over an interval, if they hold over an extension of every prefix of the interval. All these expressions can be proved with prefix induction, see [FAC11] for a definition of the prefix operator and its symbolic execution rules, which are proved here.
• Specification Safety gives a syntactic approximation as a precicate safefma?. The approximation includes always formulas, as well as chop and star formulas (lifting the definition to programs has yet to be done). The approximation is proven correct (the proof for the star-operator is quite difficult and involves several lemmas).
• An experimental rule for doing forward simulation proofs for refinement (that is also based on the prefix operator) is proved here.
• Some of the congruence rules used by KIV's simplifier are proved here.
• Some simple rules for induction (e.g. introducing a counter for an eventually) are proved here.

Applications

• RGITL is used to derive decomposition theorems for interleaved systems, as well as to apply such theorems to prove specific concurrent algorithms correct. Here is an overview over some of the applications of RGITL (including rely-guarantee theorems, decomposition of lock-freedom, specific cases studies, ...).

Back to the overview of all KIV projects.
For general informations on KIV and a download site for the whole system refer to this page.

Bibliography

[Imprint] [Data Privacy Statement] [E-Mail]