In the paper, the formal speci cation of event universes theory developed with using Coq Proof Assistant is presented. The main attention is paid on the discussion of the de nition and obtained facts. In the same time, a proof technique is not the subject of this discussion. The reader can get acquainted with the details of the proof technique, referring to the source text of Coq-scripts hosted on the GitHub, using the links provided in the text of the paper.
Inception of distributed computation technology has posed a problem of orchestration of di erent computational device operating. One of the key problem in this context is to ensure adequate responses of a computational device involved into the computation to requests of other computational devices involved into the computation too in order to ensure all these computational devices behave consistently and purposefully. Thus, it is needed to give system developers tools for speci cation and analysis of timing constraints for ensuring the consistent behaviours of hardware and software constituted the system being under design. Hence, we may claim that carefully vetted speci cation guaranteeing the system behaviour consistency in the time is the important part of a good design for a distributed system.
The speci city of the design process for distributed systems is the impossibility to apply the methods of dynamic analysis of program code to ensure its correctness. The reason for the validity of this claim is that any additional observations of the system are not possible without inclusion into the system special components, which collect the needed information but at the same time these components change the system behaviour. In some sense, we have behaviour like quantum behaviour: any observation changes essentially the system behaviour. In the situation when dynamical analysis of the system correctness is not useful, the static analysis remains the unique method for assessment of system behaviour correctness. Thus, the creation of a rigorous theory, which would ensure computer aided in developing special software for veri cation and analysis of causality speci cations for distributed systems is a very important problem for nowadays.
To solve the problem we propose to use Coq Proof Assistant [
Theory of binary relations form a mathematical basis for studying causality relationship. Therefore, we present the Coq-speci cation1 used below for the some needed for us fragment of the binary relation theory in this section.
Axiom extensionality :
8 (A B : Type) (f g : A ! B), (8 x : A, f x = g x) ! f = g.
Section EventPreliminaries.
Variable U : Type.
Definition BiRel : Type := U ! U ! Prop.
Definition Reflexive (R : BiRel) : Prop := 8 x : U, R x x. Definition Irreflexive (R : BiRel) : Prop := 8 x : U, : R x x. Definition Symmetric (R : BiRel) : Prop := 8 x y : U, R x y ! R y x. Definition Transitive (R : BiRel) : Prop :=
8 x y z : U, R x y ! R y z ! R x z.
Inductive Preorder (R : BiRel) : Prop :=
Inductive Equivalence (R : BiRel) : Prop := EquivalenceDef :
Inductive StrictOrder (R : BiRel) : Prop :=
Definition Decidable (R : BiRel) : Prop :=
8 x y : U, R x y _ : R x y.
End EventPreliminaries. 1 This speci cation is contained in https://github.com/gzholtkevych/Causality/ blob/master/Coq/EventPreliminaries.v.
Further, we give de nitions for the polymorphic identity function and composition of functions.
Definition id fA : Typeg := fun x : A ) x.
Definition compose fA B C : Typeg (f : A ! B) (g : B ! C) : A ! C := fun x : A ) g (f x).
Notation "g * f" := (compose f g)
(at level 40, left associativity) : event_scope.
Proposition 1 (id_is_leftId).
For any sets A and B and function f : A ! B, the equation idB f = f holds. Proposition 2 (id_is_rightId).
For any sets A and B and function f : A ! B, the equation f idA = f holds. Proposition 3 (compose_is_assoc ).
For any sets A, B, C, and D and functions f : A ! B, g : B ! C, and h : C ! D, the equation (h g) f = h (g f ) holds.
Definition Decidable (R : BiRel) : Prop := 8 x y : U, R x y _ : R x y. End EventPreliminaries. 3
This section introduces in the logical time model that focuses on the causality relationships between event occurrences called instants below. 3.1 Informal Meaning and Mathematical De nitions The principal causality relationship between events A and B is labelled by the sentence \the event A causes the event B". We consider informally that the semantic meaning this sentence is the statement \if the event A has not occurred then the event B cannot occur" rather than the statement \if the event A has occurred then the event B should also occur". It is evident that this semantic meaning leads to the following properties of the causality relationship
De nition 1. A set U equipped with a preorder (quasi-order) relation \ " is below called an event universe.
The statement \x y" where x; y 2 U is pronounced as \x causes y".
order, which are below called synchronisation and precedence and denoted by \+" and \<" respectively. The de nitions of these relations are the following De nition 2. Let a set U equipped with a preorder \ " be an event universe then 1. the relation x + y between any x; y 2 U (pronounced x and y are synchronous) is de ned by the condition x y and y x and called the synchronisation relation; 2. the relation x < y between any x; y 2 U (pronounced x precedes y) is de ned by the condition x y and :y x and called the precedence relation.
De nition 3. Let a set U equipped with a preorder \ " be an event universe then 1. the relation x # y between any x; y 2 U (pronounced x and y are mutually exclusive) is de ned by the condition x < y or y < x and called the mutual exclusive relation; 2. the relation x k y between any x; y 2 U (pronounced x and y are independent) is de ned by the condition :x y and :y x and called the independence relation. 3.2
Formal Model of an Event Universe and Used Notation
Now we are ready to specify the formal model of the concept of an event universe
using Coq Proof Assistant. We consider the type classes [
Class Event fA : Typeg := f universe := A ;
causality : BiRel universe ; (* Constraints *) causality_constraint (* causality is a preorder *) :
Preorder universe causality ; (* Derived relations *) synchronisation : BiRel universe :=
fun x y ) causality x y ^ causality y x ; 2 The complete code is contained in https://github.com/gzholtkevych/Causality/ blob/master/Coq/EventDefinitions.v
precedence : BiRel universe :=
fun x y ) causality x y ^ : causality y x ; exclusion : BiRel universe :=
fun x y ) precedence x y _ precedence y x ; independence : BiRel universe :=
fun x y ) : causality x y ^ : causality y x This script speci es an event universe as some type called universe equipped with a binary relations causality. The script imposes only one constraint, namely, the relation causality should be a preorder. The class de nition determines also the derived relations syncronisation, precedence, exclusion, and independence in accordance with Def. 2 and 3.
Notation "x y" (* x causes y *) := (causality x y)
(at level 70) : event_scope.
Notation "x + y" (* x and y are synchronous *) := (synchronisation x y) (at level 70) : event_scope.
Notation "x < y" (* x precedes y *) :=
(precedence x y) (at level 70) : event_scope.
Notation "x # y" (* x and y are mutually exclusive *) := (exclusion x y) (at level 70) : event_scope.
Notation "x k y" (* x and y are independent *) := (independence x y) (at level 70) : event_scope. 4
In this section, we establish several properties of the relations mentioned in the
speci cation of the type class Event. In this section, we present several simple
properties of the relations mentioned in the speci cation of type class Event.
Our presentations are the formulations of the properties as mathematical
statements. Each such a statement is equipped with the reference to the
corresponding CIC-term [
with the causality relation \ " and the synchronisation relation \ + ", precedence relation \ < ", mutual exclusion relation \ # ", and independence realtion \ k " are de ned by Def. 2 and Def. 3. 4.1
Simple Properties of Relations
Proposition 4 (synchronisation_implies_causality ). For any events x and y, x + y implies x y. Lemma 1 (synchronisation_is_reflexive ). The synchronisation relation is re exive.
Lemma 2 (synchronisation_is_transitive ). The synchronisation relation is transitive.
Lemma 3 (synchronisation_is_symmetric ). The synchronisation relation is symmetric.
Proposition 5 (synchronisation_is_equivalence ). The synchronisation relation is an equivalence.
Proposition 6 (precedence_implies_causality ). For any events x and y, x < y implies x y. Lemma 4 (precedence_is_irreflexive ). The precedence relation is irre exive.
Lemma 5 (precedence_is_transitive ). The precedence relation is transitive.
Proposition 7 (precedence_is_strictOrder ). The precedence relation is a strict order.
Proposition 8 (exclusion_is_irreflexive ). The mutual exclusion relation is irre exive. Proposition 9 (exclusion_is_symmetric ). The mutual exclusion relation is symmetric.
Proposition 10 (independence_is_irreflexive ).
The independence relation is irre exive.
Proposition 11 (independence_is_symmetric ).
The independence relation is symmetric. The next group of facts concerns the incompatibility of the relations being studied.
Proposition 12 (incompatibility_of_synchronisation_and_exclusion ). For any events x and y, at most one of the statements x + y and x#y is ful lled. Proposition 13 (incompatibility_of_synchronisation_and_independence ). For any events x and y, at most one of the statements x + y and x k y is ful lled.
Proposition 14 (incompatibility_of_exclusion_and_independence ). For any events x and y, at most one of the statements x#y and x k y is ful lled. One can note that the mutual exclusion relation between events x and y ensures either x < y or y < x but does not determine what of these precedence statements is ful lled. To determine what precedence statement is valid one can use the following fact.
Proposition 15 (causality_distinguishes_exclusion ).
For any events x and y such that x # y, x y implies x < y.
Further reasoning is aimed at identifying conditions that ensure the ful llment of the following statement called ixsDecomposition that means the following for any events x and y; x k y _ x # y _ x + y:
Theorem 1 (decidable_causality_is_equivalent_to_ixsDecomposition ). ixsDecomposition is ful lled if and only if the causality relation is decidable. 4.3
Congruence Properties In this subsection, we establish interrelations between the synchronisation relation and other relations being studied. The corresponding scripts proving these facts one can nd at https://github.com/gzholtkevych/Causality/blob/ master/Coq/EventSynchronisationCongruenceProperties.v. Proposition 16 (congruence_causality ). For any events x, x0 and y, y0 such that x + x0 and y + y0, x y implies x0 y0.
Proposition 17 (congruence_precedence ). For any events x, x0 and y, y0 such that x + x0 and y + y0, x < y implies x0 < y0.
Proposition 18 (congruence_exclusion ). For any events x, x0 and y, y0 such that x + x0 and y + y0, x # y implies x0 # y0.
Proposition 19 (congruence_independence ). For any events x, x0 and y, y0 such that x + x0 and y + y0, x k y implies x0 k y0.
Summing up the above we can state that the synchronisation relation is a congruence for all other considered relations.
In this section, we beat a path to using Category Theory3 for studying causality in distributed systems. The concept of morphism is the key to such consideration. The speci cation of type class presented below EventMorphism can be found at https://github.com/gzholtkevych/Causality/blob/master/Coq/ EventDefinitions.v.
Class EventMorphism fA B : Typeg `fEvent Ag `fEvent Bg (f : A ! B) := f arrow := f ; (* Constraints *) preserving_sync : 8 x y : A, x + y ! arrow x + arrow y ; preserving_precedence : 8 x y : A, x < y ! arrow x < arrow y In other words, an event morphism is a mapping of corresponding event sets that preserves the synchronisation and precedence relations.
github.com/gzholtkevych/Causality/blob/master/Coq/EventMorphisms.v
Proposition 20 (preserving_sync ).
For any event universes A and B, morphism f : A ! B, and events x and y of A such that x + y, the statement f x + f y is ful lled.
Proposition 21 (preserving_prec ).
For any event universes A and B, morphism f : A ! B, and events x and y of A such that x < y, the statement f x < f y is ful lled.
Proposition 22 (id_is_morphism).
For any event universe A, idA is a morphism.
Proposition 23 (composition_of_morphisms_is_morphism ).
For any event universes A, B, and C and morphisms f : A ! B and g : B ! C, g f is a morphism.
Combining Prop. 22 and 23 with Prop. 1{3 one can obtain the following theorem. Theorem 2. The class of event universes equipped with morphisms is a category.
Category-theoretic studying causality relationships was initiated in the papers
[
This paper presents the formal approach to study causality relationships in distributed systems.
has been described.
Further research and development may be focused on { the formalisation with Coq Proof Assistant of niteness conditions to emphasise the subclass of discrete event universes; { the identi cation of states related to events to try to construct a natural coalgebra for specifying the behaviour of systems being studied; { the identi cation of logical clocks for obtaining some complete and usable causality constraint speci cation language.