Documentation

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
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
    Instances For
      source
      def Rollback.RollbackCandidates (es : EventStructure) (c : Conf es) (e : es.Event) :
      Set (Conf es)

      Candidate configurations for rollback.

      Equations
      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
        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) [WellFoundedLT es.Event] {c : Conf es} {e : es.Event} (hfin : (↑c ∩ es.future e).Finite) :
          Nonempty ((t : List es.Event) × Path.ExecList es (rollbackFuture es c e) t c)

          CONJECTURE: For finite configurations, an executable list from rollback to the original configuration exists.

          source
          theorem Rollback.rollback_correctness_finite (es : EventStructure) [WellFoundedLT es.Event] {c : Conf es} {e : es.Event} (hfin : (↑c ∩ es.future e).Finite) :
          Nonempty (Path es (rollbackFuture es c e) c)

          Correctness: The original configuration c is reachable from rollback(c,e) when the future is finite and < is well-founded.

          source
          theorem Rollback.rollback_minimality (es : EventStructure) {c : Conf es} {e : es.Event} (p : Path es (rollbackFuture es c e) c) (c' : Conf es) (hredo : Configuration.enables es (↑c') e) (hsafe : ∀ x ∈ ↑c', x ∉ es.future e) (p' : Path es c' c) :
          Path.length es p ≤ Path.length es p'

          CONJECTURE: Minimality of Rollback - Any path from a candidate configuration to c is at least as long as the path from rollback(c,e) to c.