open import Tagged
open import GeneralLemmas using (Dec; _≡_)
module Backup
{Machine Msg : Set}
(_⟶Machine<_>_ : Machine → Tagged Msg → Machine → Set)
where
open import GeneralLemmas
open import Relation
data _⟶Crashy<_>_ : Maybe Machine → Tagged Msg → Maybe Machine → Set where
normal-step : ∀ {tmsg m m'} →
m ⟶Machine< tmsg > m' →
just m ⟶Crashy< tmsg > just m'
CRASH : ∀ {m} →
just m ⟶Crashy< silent > nothing
Backup = Machine × Machine
data _⟶Backup<_>_ : Backup → Tagged Msg → Backup → Set where
silent-step : ∀ {m n m'} →
just m ⟶Crashy< silent > just m' →
(m , n) ⟶Backup< silent > (m' , n)
receive-step : ∀ {m n m' msg} →
just m ⟶Crashy< receive msg > just m' →
(m , n) ⟶Backup< receive msg > (m' , m')
send-step : ∀ {m n m' msg} →
just m ⟶Crashy< send msg > just m' →
(m , n) ⟶Backup< send msg > (m' , m')
recover : ∀ {m n} →
just m ⟶Crashy< silent > nothing →
(m , n) ⟶Backup< silent > (n , n)
_⟶Machine_ : Machine → Machine → Set
m₁ ⟶Machine m₂ = ∃ λ tmsg → m₁ ⟶Machine< tmsg > m₂
module Assumptions
(active : Machine → Set)
(is-active : (m : Machine) → Dec (active m))
(active-silent-active : ∀ {m m'} →
m ⟶Machine< silent > m' → active m × active m')
(active-send-inactive : ∀ {m m' msg} →
m ⟶Machine< send msg > m' → active m × ¬ (active m'))
(inactive-receive-active : ∀ {m m' msg} →
m ⟶Machine< receive msg > m' → ¬ (active m) × active m')
where
_⟶Machine*_ = _⟶Machine_ *
_⟶MSilent_ : Machine → Machine → Set
m₁ ⟶MSilent b₂ = m₁ ⟶Machine< silent > b₂
_⟶MSilent*_ = _⟶MSilent_ *
_⟶Backup_ : Backup → Backup → Set
b₁ ⟶Backup b₂ = ∃ λ tmsg → b₁ ⟶Backup< tmsg > b₂
_⟶Backup*_ = _⟶Backup_ *
_⟶BSilent_ : Backup → Backup → Set
b₁ ⟶BSilent b₂ = b₁ ⟶Backup< silent > b₂
_⟶BSilent*_ = _⟶BSilent_ *
data IO (A : Set) : Set where
send receive : A → IO A
⟦_⟧B : ∀ {b₁ b₂} → b₁ ⟶Backup* b₂ → List (IO Msg)
⟦ [] ⟧B = []
⟦ ((silent , _) ∷ steps) ⟧B = ⟦ steps ⟧B
⟦ ((send msg , _) ∷ steps) ⟧B = send msg ∷ ⟦ steps ⟧B
⟦ ((receive msg , _) ∷ steps) ⟧B = receive msg ∷ ⟦ steps ⟧B
⟦_⟧M : ∀ {m₁ m₂} → m₁ ⟶Machine* m₂ → List (IO Msg)
⟦ [] ⟧M = []
⟦ ((silent , _) ∷ steps) ⟧M = ⟦ steps ⟧M
⟦ ((send msg , _) ∷ steps) ⟧M = send msg ∷ ⟦ steps ⟧M
⟦ ((receive msg , _) ∷ steps) ⟧M = receive msg ∷ ⟦ steps ⟧M
activeB : Backup → Set
activeB (b , _) = active b
inactiveM : Machine → Set
inactiveM m = ¬ active m
inactiveB : Backup → Set
inactiveB b = ¬ activeB b
soundness : ∀ {m₁ m₂ b₁}
(mtrace : m₁ ⟶Machine* m₂) →
∃₂ λ b₂ (btrace : (m₁ , b₁) ⟶Backup* (m₂ , b₂)) →
⟦ btrace ⟧B ≡ ⟦ mtrace ⟧M
soundness [] = _ , [] , refl
soundness ((silent , st) ∷ mtrace) =
let (b₂ , btrace , eq) = soundness mtrace
in b₂ , (silent , silent-step (normal-step st)) ∷ btrace , eq
soundness ((send msg , st) ∷ mtrace) =
let (b₂ , btrace , eq) = soundness mtrace
in b₂ , (send msg , send-step (normal-step st)) ∷ btrace , cong (_∷_ _) eq
soundness ((receive msg , st) ∷ mtrace) =
let (b₂ , btrace , eq) = soundness mtrace
in b₂ , (receive msg , receive-step (normal-step st)) ∷ btrace , cong (_∷_ _) eq
thread-crashes : ∀ {m₁ m₂} → m₁ ⟶Backup* m₂ → Set
thread-crashes [] = ⊥
thread-crashes (_∷_ (.silent , silent-step x) s) = thread-crashes s
thread-crashes (_∷_ (._ , receive-step x) s) = ⊥
thread-crashes (_∷_ (._ , send-step x) s) = ⊥
thread-crashes (_∷_ (.silent , recover x) s) = ⊤
does-thread-crash : ∀ {m₁ m₂} → (s : m₁ ⟶Backup* m₂) → Dec (thread-crashes s)
does-thread-crash [] = no (λ z → z)
does-thread-crash (_∷_ (.silent , silent-step x) s) = does-thread-crash s
does-thread-crash (_∷_ (._ , receive-step x) s) = no (λ z → z)
does-thread-crash (_∷_ (._ , send-step x) s) = no (λ z → z)
does-thread-crash (_∷_ (.silent , recover x) s) = yes tt
fast-forward-to-crash : ∀ {m₁ m₂ b₁ b₂ n} →
(s : (m₁ , b₁) ⟶Backup* (m₂ , b₂)) → thread-crashes s → *length s ≤ n →
∃ λ (s' : (b₁ , b₁) ⟶Backup* (m₂ , b₂)) → (¬ thread-crashes s') ×
(⟦ s ⟧B ≡ ⟦ s' ⟧B) ×
(*length s' ≤ n)
fast-forward-to-crash [] ()
fast-forward-to-crash (_∷_ (.silent , silent-step x) s) tc (s≤s len≤n) =
let (s' , no-crash) = fast-forward-to-crash s tc (≤-steps 1 len≤n)
in s' , no-crash
fast-forward-to-crash (_∷_ (._ , receive-step x) s) () len≤n
fast-forward-to-crash (_∷_ (._ , send-step x) s) () len≤n
fast-forward-to-crash (_∷_ (.silent , recover x) s) tc (s≤s len≤n) with does-thread-crash s
... | yes it-does = fast-forward-to-crash s it-does (≤-steps 1 len≤n)
... | no it-doesn't = s , it-doesn't , refl , ≤-steps 1 len≤n
fast-forward : ∀ {m₂ b₁ b₂ n} →
(s : (b₁ , b₁) ⟶Backup* (m₂ , b₂)) → *length s ≤ n →
∃ λ (s' : (b₁ , b₁) ⟶Backup* (m₂ , b₂)) → (¬ thread-crashes s') ×
(⟦ s ⟧B ≡ ⟦ s' ⟧B) ×
(*length s' ≤ n)
fast-forward s len≤n with does-thread-crash s
... | yes it-does = fast-forward-to-crash s it-does len≤n
... | no it-doesn't = s , it-doesn't , refl , len≤n
completeness-inactive : ∀ {m₂ b₁ b₂} n
(bs : (b₁ , b₁) ⟶Backup* (m₂ , b₂)) → *length bs ≤ n →
inactiveB (b₁ , b₁) →
∃ λ (ms : b₁ ⟶Machine* m₂) → ⟦ bs ⟧B ≡ ⟦ ms ⟧M
completeness-active : ∀ {m₁ m₂ b₁ b₂} n
(bs : (m₁ , b₁) ⟶Backup* (m₂ , b₂)) → *length bs ≤ n →
activeB (m₁ , b₁) → ¬ thread-crashes bs →
(backup : b₁ ⟶MSilent* m₁) →
∃ λ (ms : m₁ ⟶Machine* m₂) → ⟦ bs ⟧B ≡ ⟦ ms ⟧M
completeness-inactive zero [] z≤n inactive = [] , refl
completeness-inactive zero (_∷_ x steps) () inactive
completeness-inactive (suc n) [] z≤n inactive = [] , refl
completeness-inactive (suc n) (_∷_ (.silent , silent-step (normal-step s)) steps) (s≤s len≤n) inactive =
⊥-elim (inactive (proj₁ (active-silent-active s)))
completeness-inactive (suc n) (_∷_ (._ , receive-step (normal-step s)) steps) (s≤s len≤n) inactive =
let steps' , ¬crash , eq , len'≤n = fast-forward steps len≤n
msteps , eq' = completeness-active n steps' len'≤n (proj₂ (inactive-receive-active s)) ¬crash []
in (receive _ , s) ∷ msteps , cong (_∷_ _) (trans eq eq')
completeness-inactive (suc n) (_∷_ (._ , send-step (normal-step s)) steps) (s≤s len≤n) inactive =
⊥-elim (inactive (proj₁ (active-send-inactive s)))
completeness-inactive (suc n) (_∷_ (.silent , recover CRASH) steps) (s≤s len≤n) inactive =
completeness-inactive n steps len≤n inactive
completeness-active zero [] z≤n active ¬crash backup = [] , refl
completeness-active zero (_∷_ x steps) () active ¬crash backup
completeness-active (suc n) [] z≤n active ¬crash backup = [] , refl
completeness-active (suc n) (_∷_ (.silent , silent-step (normal-step s)) steps) (s≤s len≤n) active ¬crash backup =
let msteps , eq = completeness-active n steps len≤n (proj₂ (active-silent-active s)) ¬crash (backup *++ (s ∷ []))
in (silent , s) ∷ msteps , eq
completeness-active (suc n) (_∷_ (._ , receive-step (normal-step s)) steps) (s≤s len≤n) active ¬crash backup =
⊥-elim (proj₁ (inactive-receive-active s) active)
completeness-active (suc n) (_∷_ (._ , send-step (normal-step s)) steps) (s≤s len≤n) active ¬crash backup =
let msteps , eq = completeness-inactive n steps len≤n (proj₂ (active-send-inactive s))
in (send _ , s) ∷ msteps , cong (_∷_ _) eq
completeness-active (suc n) (_∷_ (.silent , recover CRASH) steps) (s≤s len≤n) active ¬crash backup =
⊥-elim (¬crash tt)
completeness : ∀ {b₁ m₂ b₂}
(bs : (b₁ , b₁) ⟶Backup* (m₂ , b₂)) →
∃ λ (ms : b₁ ⟶Machine* m₂) →
⟦ bs ⟧B ≡ ⟦ ms ⟧M
completeness {b₁ = b₁} bs with is-active b₁
... | yes it-is = let bs' , ¬crash , eq , len≤n = fast-forward bs ≤-refl
ms , eq' = completeness-active (*length bs') bs' ≤-refl it-is ¬crash []
in ms , trans eq eq'
... | no it's-not = completeness-inactive (*length bs) bs ≤-refl it's-not