EventStructures.Rollback

source

def Rollback.isRollback (es : EventStructure) (c : Conf es) (e : es.Event) (m : Conf es) :

Prop

A rollback of event e on configuration c is a maximal configuration m with m ⊆ c and e ∉ m.

Equations

Rollback.isRollback es c e m = (↑m ⊆ ↑c ∧ e ∉ ↑m ∧ ∀ (m' : Conf es), ↑m' ⊆ ↑c → e ∉ ↑m' → ↑m ⊆ ↑m' → ↑m' ⊆ ↑m)

Instances For

source

def Rollback.Rollbacks (es : EventStructure) (c : Conf es) (e : es.Event) :

Set (Conf es)

The set of all rollbacks of event e on configuration c.

Equations

Rollback.Rollbacks es c e = {m : Conf es | Rollback.isRollback es c e m}

Instances For

source

def Rollback.RollbackCandidates (es : EventStructure) (c : Conf es) (e : es.Event) :

Set (Conf es)

Candidate configurations for rollback.

Equations

Rollback.RollbackCandidates es c e = {m : Conf es | ↑m ⊆ ↑c ∧ e ∉ ↑m}

Instances For

source

@[simp]

theorem Rollback.rollback_subset (es : EventStructure) {c : Conf es} {e : es.Event} {m : Conf es} (h : isRollback es c e m) :

↑m ⊆ ↑c

source

@[simp]

theorem Rollback.rollback_not_mem (es : EventStructure) {c : Conf es} {e : es.Event} {m : Conf es} (h : isRollback es c e m) :

e ∉ ↑m

source

theorem Rollback.rollback_maximal (es : EventStructure) {c : Conf es} {e : es.Event} {m : Conf es} (h : isRollback es c e m) (m' : Conf es) :

↑m' ⊆ ↑c → e ∉ ↑m' → ↑m ⊆ ↑m' → ↑m' ⊆ ↑m

source

theorem Rollback.isRollback_iff_maximal (es : EventStructure) {c : Conf es} {e : es.Event} {m : Conf es} :

isRollback es c e m ↔ m ∈ RollbackCandidates es c e ∧ ∀ m' ∈ RollbackCandidates es c e, ↑m ⊆ ↑m' → ↑m' ⊆ ↑m

source

theorem Rollback.rollback_subset_future (es : EventStructure) {c : Conf es} {e : es.Event} {m : Conf es} (h : isRollback es c e m) :

↑m ⊆ ↑c \ es.future e

source

theorem Rollback.rollback_future_isConf (es : EventStructure) {c : Conf es} {e : es.Event} :

isConf es (↑c \ es.future e)

Removing the future of e from a configuration keeps it a configuration.

source

def Rollback.rollbackFuture (es : EventStructure) (c : Conf es) (e : es.Event) :

Conf es

The canonical rollback configuration: remove all events causally after e.

Equations

Rollback.rollbackFuture es c e = ⟨↑c \ es.future e, ⋯⟩

Instances For

source

@[simp]

theorem Rollback.rollbackFuture_val (es : EventStructure) (c : Conf es) (e : es.Event) :

↑(rollbackFuture es c e) = ↑c \ es.future e

source

@[simp]

theorem Rollback.rollbackFuture_mem (es : EventStructure) {c : Conf es} {e x : es.Event} :

x ∈ ↑(rollbackFuture es c e) ↔ x ∈ ↑c ∧ x ∉ es.future e

source

theorem Rollback.rollback_redoable (es : EventStructure) {c : Conf es} {e : es.Event} (he : e ∈ ↑c) :

Configuration.enables es (↑(rollbackFuture es c e)) e

Redoability: e is enabled in rollback(c,e) when e ∈ c.

source

theorem Rollback.rollback_causal_safety (es : EventStructure) {c : Conf es} {e x : es.Event} :

x ∈ ↑(rollbackFuture es c e) → x ∉ es.future e

Causal safety: Rollback removes exactly the causal consequences of e.

source

theorem Rollback.rollback_future (es : EventStructure) {c : Conf es} {e : es.Event} :

isRollback es c e (rollbackFuture es c e)

The canonical rollback is a rollback for c and e.

source

@[simp]

theorem Rollback.rollback_eq_future (es : EventStructure) {c : Conf es} {e : es.Event} {m : Conf es} (h : isRollback es c e m) :

↑m = ↑c \ es.future e

Any rollback coincides with the canonical rollback.

source

theorem Rollback.rollback_unique (es : EventStructure) {c : Conf es} {e : es.Event} {m₁ m₂ : Conf es} (h₁ : isRollback es c e m₁) (h₂ : isRollback es c e m₂) :

m₁ = m₂

Rollbacks are unique when they exist.

source

theorem Rollback.rollback_maximum (es : EventStructure) {c : Conf es} {e : es.Event} {m : Conf es} (h : isRollback es c e m) (m' : Conf es) :

m' ∈ RollbackCandidates es c e → ↑m' ⊆ ↑m

The rollback is the maximum element among rollback candidates.

source

theorem Rollback.event_enabled_when_past_present (es : EventStructure) {c : Conf es} {e x : es.Event} (hx : x ∈ ↑c ∩ es.future e) (c' : Conf es) (hpast : ∀ y < x, y ∈ ↑c ∩ es.future e → y ∈ ↑c') (hbase : ↑(rollbackFuture es c e) ⊆ ↑c') (hconf : ↑c' ⊆ ↑c) :

Configuration.enables es (↑c') x

Helper: An event in the future is enabled in a partial configuration that contains its strict past and is consistent.

source

theorem Rollback.execList_exists_finite (es : EventStructure) [DecidableEventStructure es] {c : Conf es} {e : es.Event} (cF : Finset es.Event) (hcF : ∀ (x : es.Event), x ∈ cF ↔ x ∈ ↑c) :

Nonempty ((t : List es.Event) × Path.ExecList es (rollbackFuture es c e) t c)

Constructive: given a Finset representation cF of the underlying configuration c, there is an executable list from the rollback configuration to c. Uses decidable equality and decidable strict order on events.

source

theorem Rollback.rollback_correctness_finite (es : EventStructure) [DecidableEventStructure es] {c : Conf es} {e : es.Event} (cF : Finset es.Event) (hcF : ∀ (x : es.Event), x ∈ cF ↔ x ∈ ↑c) :

Nonempty (Path es (rollbackFuture es c e) c)

Correctness: the original configuration c is reachable from rollback(c,e) when c.1 admits a Finset representation.

source

theorem Rollback.rollback_minimality (es : EventStructure) [DecidableEq es.Event] {c : Conf es} {e : es.Event} {c' : Conf es} (_hredo : Configuration.enables es (↑c') e) (hsafe : ∀ x ∈ ↑c', x ∉ es.future e) (p' : Path es c' c) :

(↑c ∩ es.future e).ncard ≤ Path.length es p'

Minimality of Rollback - Any path from a redo-candidate configuration c' to c is at least as long as the number of events in c causally after e.