-
Notifications
You must be signed in to change notification settings - Fork 1
/
fairness.v
170 lines (139 loc) · 5.86 KB
/
fairness.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
From stdpp Require Import option.
From Paco Require Import paco1 paco2 pacotac.
From trillium.fairness Require Export inftraces.
Record FairModel : Type := {
fmstate:> Type;
fmstate_eqdec: EqDecision fmstate;
fmstate_inhabited: Inhabited fmstate;
fmrole: Type;
fmrole_eqdec: EqDecision fmrole;
fmrole_countable: Countable fmrole;
fmrole_inhabited: Inhabited fmrole;
fmtrans: fmstate -> option fmrole -> fmstate -> Prop;
live_roles: fmstate -> gset fmrole;
fm_live_spec: forall s ρ s', fmtrans s (Some ρ) s' -> ρ ∈ live_roles s;
}.
#[global] Existing Instance fmrole_eqdec.
#[global] Existing Instance fmrole_countable.
#[global] Existing Instance fmrole_inhabited.
#[global] Existing Instance fmstate_inhabited.
(* Basically, soundness of the logic and the lemmas above tell us that we have a program
trace and a model trace which are related by traces_match labels_math!
We now prove that this relation transports the properties we care about; the first
place of which is fairness.
*)
(* Definition of fairness for both kinds of traces *)
Definition extrace Λ := trace (cfg Λ) (olocale Λ).
Section exec_trace.
Context {Λ : language}.
Context `{EqDecision (locale Λ)}.
Definition locale_enabled (ζ : locale Λ) (c: cfg Λ) :=
∃ e, from_locale c.1 ζ = Some e ∧ to_val e = None.
Definition fair_ex ζ (extr: extrace Λ): Prop :=
forall n, pred_at extr n (λ c _, locale_enabled ζ c) ->
∃ m, pred_at extr (n+m) (λ c _, ¬locale_enabled ζ c)
∨ pred_at extr (n+m) (λ _ otid, otid = Some (Some ζ)).
Lemma fair_ex_after ζ tr tr' k:
after k tr = Some tr' ->
fair_ex ζ tr -> fair_ex ζ tr'.
Proof.
intros Haf Hf n Hp.
have Hh:= Hf (k+n).
have Hp': pred_at tr (k + n) (λ (c : cfg Λ) (_ : option (olocale Λ)), locale_enabled ζ c).
{ rewrite (pred_at_sum _ k) Haf /= //. }
have [m Hm] := Hh Hp'. exists m.
by rewrite <- Nat.add_assoc, !(pred_at_sum _ k), Haf in Hm.
Qed.
Lemma fair_ex_cons tid c tid' r:
fair_ex tid (c -[tid']-> r) -> fair_ex tid r.
Proof. intros H. by eapply (fair_ex_after tid (c -[tid']-> r) r 1). Qed.
CoInductive extrace_valid: extrace Λ -> Prop :=
| extrace_valid_singleton c: extrace_valid ⟨c⟩
| extrace_valid_cons c oζ tr:
locale_step c oζ (trfirst tr) ->
extrace_valid tr →
extrace_valid (c -[oζ]-> tr).
Lemma to_trace_preserves_validity ex iex:
extrace_valid (to_trace (trace_last ex) iex) -> valid_exec ex -> valid_inf_exec ex iex.
Proof.
revert ex iex. cofix CH. intros ex iex Hexval Hval.
rewrite (trace_unfold_fold (to_trace _ _)) in Hexval.
destruct iex as [|[??] iex]; first by econstructor. cbn in Hexval.
inversion Hexval. simplify_eq.
econstructor; try done.
- by destruct iex as [|[??]?].
- apply CH; eauto. econstructor; try done. by destruct iex as [|[??]?].
Qed.
Lemma from_trace_preserves_validity (extr: extrace Λ) ex:
extrace_valid extr ->
valid_exec ex ->
trace_last ex = trfirst extr ->
valid_inf_exec ex (from_trace extr).
Proof.
revert ex extr. cofix CH. intros ex extr Hexval Hval Heq.
rewrite (inflist_unfold_fold (from_trace extr)). destruct extr as [c|c tid tr]; cbn;
first by econstructor.
inversion Hexval; simplify_eq; econstructor; eauto. apply CH; eauto.
by econstructor.
Qed.
Lemma from_trace_preserves_validity_singleton (extr: extrace Λ):
extrace_valid extr ->
valid_inf_exec (trace_singleton (trfirst extr)) (from_trace extr).
Proof.
intros ?. eapply from_trace_preserves_validity; eauto. econstructor.
Qed.
End exec_trace.
Definition mtrace (M:FairModel) := trace M (option M.(fmrole)).
Section model_traces.
Context `{M: FairModel}.
Definition role_enabled_model ρ (s: M) := ρ ∈ M.(live_roles) s.
Definition fair_model_trace ρ (mtr: mtrace M): Prop :=
forall n, pred_at mtr n (λ δ _, role_enabled_model ρ δ) ->
∃ m, pred_at mtr (n+m) (λ δ _, ¬role_enabled_model ρ δ)
∨ pred_at mtr (n+m) (λ _ ℓ, ℓ = Some (Some ρ)).
Lemma fair_model_trace_after ℓ tr tr' k:
after k tr = Some tr' ->
fair_model_trace ℓ tr -> fair_model_trace ℓ tr'.
Proof.
intros Haf Hf n Hp.
have Hh:= Hf (k+n).
have Hp': pred_at tr (k + n) (λ δ _, role_enabled_model ℓ δ).
{ rewrite (pred_at_sum _ k) Haf /= //. }
have [m Hm] := Hh Hp'. exists m.
by rewrite <- Nat.add_assoc, !(pred_at_sum _ k), Haf in Hm.
Qed.
Lemma fair_model_trace_cons ℓ δ ℓ' r:
fair_model_trace ℓ (δ -[ℓ']-> r) -> fair_model_trace ℓ r.
Proof. intros Hfm. by eapply (fair_model_trace_after ℓ _ r 1) =>//. Qed.
Lemma fair_model_trace_cons_forall δ ℓ' r:
(∀ ℓ, fair_model_trace ℓ (δ -[ℓ']-> r)) -> (∀ ℓ, fair_model_trace ℓ r).
Proof. eauto using fair_model_trace_cons. Qed.
Inductive mtrace_valid_ind (mtrace_valid_coind: mtrace M -> Prop) :
mtrace M -> Prop :=
| mtrace_valid_singleton δ: mtrace_valid_ind _ ⟨δ⟩
| mtrace_valid_cons δ ℓ tr:
fmtrans _ δ ℓ (trfirst tr) ->
mtrace_valid_coind tr →
mtrace_valid_ind _ (δ -[ℓ]-> tr).
Definition mtrace_valid := paco1 mtrace_valid_ind bot1.
Lemma mtrace_valid_mono :
monotone1 mtrace_valid_ind.
Proof.
unfold monotone1. intros x0 r r' IN LE.
induction IN; try (econstructor; eauto; done).
Qed.
Hint Resolve mtrace_valid_mono : paco.
Lemma mtrace_valid_after (mtr mtr' : mtrace M) k :
after k mtr = Some mtr' → mtrace_valid mtr → mtrace_valid mtr'.
Proof.
revert mtr mtr'.
induction k; intros mtr mtr' Hafter Hvalid.
{ destruct mtr'; simpl in *; by simplify_eq. }
punfold Hvalid.
inversion Hvalid as [|??? Htrans Hval']; simplify_eq.
eapply IHk; [done|].
by inversion Hval'.
Qed.
End model_traces.
Global Hint Resolve fair_model_trace_cons: core.
Global Hint Resolve mtrace_valid_mono : paco.