Configuration families

A configuration family is a collection of sets of events that are considered to be configurations. Paths, traces, computations, rollback and replay are stated at the level of configuration families.

structure ConfFamily (Label : Type u_1) : Type (max u_1 (u_2 + 1))

Events, the sets of them that count as configurations, and labels.

• Event : Type u_2
• Config : Set self.Event → Prop
• label : self.Event → Label
• empty_mem : self.Config ∅
• secured {x y : Set self.Event} : self.Config x → self.Config y → y ⊆ x → (x \ y).Finite → x ≠ y → ∃ e ∈ x \ y, self.Config (x \ {e})

  A finite gap between configurations closes one event at a time.

def ConfFamily.Conf {L : Type u_1} (F : ConfFamily L) : Type u_2

Configurations of F.

Equations

• F.Conf = { X : Set F.Event // F.Config X }

def ConfFamily.FinConf {L : Type u_1} (F : ConfFamily L) : Type u_2

Finite configurations of F.

Equations

• F.FinConf = { X : Finset F.Event // F.Config ↑X }

def ConfFamily.empty {L : Type u_1} (F : ConfFamily L) : F.Conf

The empty configuration.

Equations

• F.empty = ⟨∅, ⋯⟩

def ConfFamily.enables {L : Type u_1} (F : ConfFamily L) (c : Set F.Event) (e : F.Event) : Prop

c enables e when both c and c ∪ {e} are configurations.

Equations

• F.enables c e = (F.Config c ∧ F.Config (c ∪ {e}))

theorem ConfFamily.enables_conf {L : Type u_1} {F : ConfFamily L} {c : Set F.Event} {e : F.Event} (h : F.enables c e) : F.Config c

theorem ConfFamily.enables_extension {L : Type u_1} {F : ConfFamily L} {c : Set F.Event} {e : F.Event} (h : F.enables c e) : F.Config (c ∪ {e})

theorem ConfFamily.enables_of {L : Type u_1} {F : ConfFamily L} {c : Set F.Event} {e : F.Event} (hc : F.Config c) (hx : F.Config (c ∪ {e})) : F.enables c e

theorem ConfFamily.union_pair_comm {α : Type u_2} (s : Set α) (a b : α) : s ∪ {a} ∪ {b} = s ∪ {b} ∪ {a}

Singleton extensions commute.

def ConfFamily.Indep {L : Type u_1} (F : ConfFamily L) (c : Set F.Event) (e₁ e₂ : F.Event) : Prop

Coinitial independence: separately and jointly extendable. It is relative to c, since in a general event structure two events may be independent at one configuration and not at another.

Equations

• F.Indep c e₁ e₂ = (e₁ ≠ e₂ ∧ F.enables c e₁ ∧ F.enables c e₂ ∧ F.Config (c ∪ {e₁} ∪ {e₂}))

theorem ConfFamily.Indep.symm {L : Type u_1} {F : ConfFamily L} {c : Set F.Event} {e₁ e₂ : F.Event} (h : F.Indep c e₁ e₂) : F.Indep c e₂ e₁

Independence is symmetric.

theorem ConfFamily.Indep.irrefl {L : Type u_1} {F : ConfFamily L} {c : Set F.Event} {e : F.Event} : ¬F.Indep c e e

Independence is irreflexive.

def ConfFamily.compat {L : Type u_1} (F : ConfFamily L) (e₁ e₂ : F.Event) : Prop

The binary consistency induced by the family.

Equations

• F.compat e₁ e₂ = ∃ (c : Set F.Event), F.Config c ∧ e₁ ∈ c ∧ e₂ ∈ c