Commit 1c9d9e9b authored by Hai Dang's avatar Hai Dang
Browse files

Remove linearizability specs

parent cee441f9
......@@ -112,10 +112,6 @@ theories/examples/graph/graph.v
theories/examples/graph/graph_extend.v
theories/examples/graph/ghost.v
theories/examples/graph/spec.v
## Linearizability Specs
theories/examples/linearizability/spec.v
theories/examples/linearizability/events_ghost.v
theories/examples/linearizability/event_list_helper.v
## Message-Passing
theories/examples/mp/code.v
......@@ -134,7 +130,6 @@ theories/examples/circ_buff/proof_gps.v
theories/examples/stack/spec_na.v
theories/examples/stack/spec_per_elem.v
theories/examples/stack/spec_graph.v
theories/examples/stack/spec_lin.v
theories/examples/stack/code_na.v
theories/examples/stack/code_treiber.v
theories/examples/stack/code_elimination.v
......@@ -149,21 +144,17 @@ theories/examples/queue/spec_per_elem.v
theories/examples/queue/code_ms.v
theories/examples/queue/code_hw.v
theories/examples/queue/spec_graph.v
theories/examples/queue/spec_lin.v
theories/examples/queue/proof_ms_gps.v
theories/examples/queue/proof_ms_graph.v
theories/examples/queue/proof_hw_graph.v
theories/examples/queue/proof_per_elem_graph.v
theories/examples/queue/proof_mp_graph.v
theories/examples/queue/proof_mp_lin.v
theories/examples/queue/proof_exchange_lin.v
## Chase-Lev Double-ended Queue
theories/examples/chase_lev/code.v
## Exchanger
theories/examples/exchanger/code.v
theories/examples/exchanger/spec_graph.v
theories/examples/exchanger/spec_graph_piggyback.v
theories/examples/exchanger/spec_lin.v
theories/examples/exchanger/spec_graph_resource.v
theories/examples/exchanger/proof_graph_piggyback.v
theories/examples/exchanger/proof_graph.v
......
Require Import stdpp.namespaces.
From iris.algebra Require Import auth frac_auth gset gmap.
From iris.bi Require Import lib.atomic weakestpre lib.fractional.
From iris.proofmode Require Import tactics.
From gpfsl.lang Require Import notation.
From gpfsl.base_logic Require Import vprop.
From gpfsl.logic Require Import atomics logatom invariants proofmode.
From gpfsl.logic Require Import new_delete.
From gpfsl.examples.graph Require Import graph.
From gpfsl.examples.linearizability Require Import spec events_ghost event_list_helper.
From gpfsl.examples.exchanger Require Import code.
Require Import iris.prelude.options.
Inductive ExchangerInput := ExchangerInput_Exchange (v : Z).
Inductive ExchangerOutput :=
| ExchangerOutput_Exchange (v : Z)
| ExchangerOutput_Cancel.
Instance ExchangerInput_eq_dec : EqDecision ExchangerInput.
Proof. solve_decision. Qed.
Instance ExchangerInput_count : Countable ExchangerInput.
Proof.
refine (inj_countable
(λ v, match v with
| ExchangerInput_Exchange v => v
end)
(λ s, match s with
| v => Some $ ExchangerInput_Exchange v
end) _); by intros [].
Qed.
Instance ExchangerOutput_eq_dec : EqDecision ExchangerOutput.
Proof. solve_decision. Qed.
Instance ExchangerOutput_count : Countable ExchangerOutput.
Proof.
refine (inj_countable
(λ v, match v with
| ExchangerOutput_Exchange v => inl v
| ExchangerOutput_Cancel => inr ()
end)
(λ s, match s with
| inl v => Some $ ExchangerOutput_Exchange v
| inr () => Some ExchangerOutput_Cancel
end) _); by intros [].
Qed.
Notation exchanger_event := (hist_event ExchangerInput ExchangerOutput).
(* Abstract representation of exchanger.
In the exchanger's history, a successful exchange events pair must be adjacent.
The events in the pair refers to the other events i.e.
- 1st event's output value is the 2nd event's input value (vR) and vice versa
(vL); and
- 1st event's output view is larger than 2nd event's input view (ViR ⊑ VoL) and
vice versa (ViL ⊑ VoR).
However, we can't express this in the `run` relation because it only takes a
single event. To overcome this, we use the abstract representation type of
`option ((Z * view) * (Z * view))`. The 1st event in the pair initiates the state to
`Some ((vL, ViL), (vR, ViR))` and the 2nd event resets it to `None`. Using the
`Some` state, we can ensure that the exchange pair agrees on the exchanged
values and views in the `run` relation. An interesting point of this approach
is that the `Some` state is not observable. We can encode this fact by
asserting that the history interpretation always ends up in the `None` state,
meaning that the exchange events are always added in pairs. *)
Inductive exchanger_run : (he : exchanger_event) (s s' : option ((Z * view) * (Z * view))), Prop :=
| exchanger_run_ExchangeL vL vR ViL ViR VoL : (* return the future input and remember it *)
ViR VoL
exchanger_run
(mkHistEvent (ExchangerInput_Exchange vL) (ExchangerOutput_Exchange vR) ViL VoL)
None
(Some ((vL, ViL), (vR, ViR)))
| exchanger_run_ExchangeR vL vR ViL ViR VoR :
ViL VoR
exchanger_run
(mkHistEvent (ExchangerInput_Exchange vR) (ExchangerOutput_Exchange vL) ViR VoR)
(Some ((vL, ViL), (vR, ViR)))
None
| exchanger_run_Cancelled v Vi Vo :
exchanger_run (mkHistEvent (ExchangerInput_Exchange v) ExchangerOutput_Cancel Vi Vo) None None
.
Notation exchanger_event_map Eid := (event_map Eid ExchangerInput ExchangerOutput).
Notation exchanger_history := (interp_history None exchanger_run).
Section exchanger_resources.
Context {Σ} (P : Z vProp Σ) (Q : Z Z bool).
Notation vProp := (vProp Σ).
Definition exchanger_resources (x : option (Z * view)) : vProp :=
match x with
| Some _ => False%I
| None => emp
end.
Instance exchanger_resources_objective x : Objective (exchanger_resources x).
Proof. destruct x; apply _. Qed.
Definition ExchangerInputResource input : vProp :=
match input with
| ExchangerInput_Exchange v => v >= 0 P v
end.
(* exchange the resource only if a certain condition (Q) on the pair is satisfied *)
Definition ExchangerOutputResource (he : exchanger_event) (r : val) : vProp :=
match (he.(he_input), he.(he_output)) with
| (ExchangerInput_Exchange v, ExchangerOutput_Exchange v') =>
r = #v' v' >= 0
(if Q v v' then P v' else P v)%I
| (ExchangerInput_Exchange v, ExchangerOutput_Cancel) =>
r = #-1 P v
end.
End exchanger_resources.
Record exchanger_spec `{!noprolG Σ}
{P : Z vProp Σ} {Q : Z Z bool} := ExchangerSpec {
(* types *)
exchanger_Eid : Type;
exchanger_Eid_inhab : Inhabited exchanger_Eid;
exchanger_Eid_eqdec : EqDecision exchanger_Eid;
exchanger_Eid_count : Countable exchanger_Eid;
(* operations *)
exchanger_new : val;
exchanger_exchange : val;
exchanger_code (obj : val) (input : ExchangerInput) : expr :=
match input with
| ExchangerInput_Exchange v => exchanger_exchange [ obj; #v]%E
end;
(* predicates *)
exchanger_handle : lin_spec_handleT exchanger_Eid ExchangerInput ExchangerOutput;
exchanger_handle_info :
lin_spec_handle_infoT
exchanger_Eid ExchangerInput ExchangerOutput
(option ((Z * view) * (Z * view))) None exchanger_run
exchanger_handle;
exchanger_handle_split : lin_spec_handle_splitT exchanger_Eid ExchangerInput ExchangerOutput exchanger_handle;
exchanger_handle_join : lin_spec_handle_joinT exchanger_Eid ExchangerInput ExchangerOutput exchanger_handle;
exchanger_handle_seen_events : lin_spec_handle_seen_eventsT exchanger_Eid ExchangerInput ExchangerOutput exchanger_handle;
exchanger_handle_orders : lin_spec_handle_ordersT exchanger_Eid ExchangerInput ExchangerOutput exchanger_handle;
(* specs *)
exchanger_exchange_spec obj γ N f events owned orders tid v (V : view) :
lin_spec_operation_specT
exchanger_Eid ExchangerInput ExchangerOutput
exchanger_handle
(ExchangerInputResource P)
(ExchangerOutputResource P Q)
obj γ N f events owned orders tid V
exchanger_code
(ExchangerInput_Exchange v);
}.
Arguments exchanger_spec {_ _} _ _ : assert.
Existing Instances exchanger_Eid_inhab exchanger_Eid_eqdec exchanger_Eid_count.
Program Definition exchanger_linearizable `{!noprolG Σ}
{P : Z vProp Σ} {Q : Z Z bool}
(exchanger : exchanger_spec P Q) : linearizability_spec := {|
lin_spec_Eid := exchanger.(exchanger_Eid);
lin_spec_Input := ExchangerInput;
lin_spec_Output := ExchangerOutput;
lin_spec_AObj := option ((Z * view) * (Z * view));
lin_spec_init_aobj := None;
lin_spec_run_event := exchanger_run;
lin_spec_handle := exchanger.(exchanger_handle);
lin_spec_input_resource := ExchangerInputResource P;
lin_spec_output_resource := ExchangerOutputResource P Q;
lin_spec_handle_info := exchanger.(exchanger_handle_info);
lin_spec_handle_split := exchanger.(exchanger_handle_split);
lin_spec_handle_join := exchanger.(exchanger_handle_join);
lin_spec_handle_seen_events := exchanger.(exchanger_handle_seen_events);
lin_spec_handle_orders := exchanger.(exchanger_handle_orders);
lin_spec_code := exchanger.(exchanger_code);
|}.
Next Obligation. destruct input, exchanger; auto. Qed.
This diff is collapsed.
Require Import gpfsl.examples.sflib.
From iris.algebra Require Import agree frac_auth gset gmap.
From iris.bi Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Import own.
From gpfsl.algebra Require Import to_agree.
From gpfsl.base_logic Require Import vprop.
From gpfsl.examples.graph Require Import map_helper.
From gpfsl.examples.linearizability Require Import spec.
Section hist_camera.
Context `{Countable Eid} {Input Output : Type}.
Notation EidO := (leibnizO Eid).
Notation eventO := (leibnizO (hist_event Input Output)).
Definition event_mapR := gmapUR Eid (agreeR eventO).
Definition event_setR := gset_disjR Eid.
Definition event_orderR := gsetUR (prodO EidO EidO).
Definition historyR :=
prodR (prodR (frac_authR event_mapR)
(frac_authR event_setR))
(frac_authR event_orderR).
Notation event_map := (event_map Eid Input Output).
Notation event_set := (gset Eid).
Notation event_order := (gset (Eid * Eid)).
Notation event_mapO := (gmap Eid eventO).
Notation event_setO := (gset EidO).
Implicit Types (events eventsM : event_map)
(owned ownedM : event_set)
(orders ordersM : event_order).
Definition wrap_events (events : event_map) : event_mapR := to_agreeM events.
(* owned: events created by this thread and its joined descendant *)
Definition frag_events f events owned orders : historyR :=
(F{f} (wrap_events events), F{f} (GSet owned), F{f} orders).
Definition auth_events eventsM ordersM : historyR :=
(F (wrap_events eventsM), F (GSet (dom event_set eventsM)), F ordersM).
Lemma event_map_op_join events1 events2 :
(wrap_events events1 wrap_events events2)
wrap_events events1 wrap_events events2 wrap_events (events1 events2).
Proof. apply to_agreeM_op_valid. Qed.
Lemma event_map_op_join_sym events1 events2 :
(wrap_events events1 wrap_events events2)
events1 events2 = events2 events1.
Proof. apply to_agreeM_valid_union. Qed.
End hist_camera.
Arguments event_mapR _ {_ _} _ _ : assert.
Arguments historyR _ {_ _} _ _ : assert.
Class historyG Σ (Eid Input Output : Type) `{Countable Eid} := {
history_inG :> inG Σ (historyR Eid Input Output);
}.
Definition historyΣ (Eid Input Output : Type) `{Countable Eid} : gFunctors :=
#[GFunctor (historyR Eid Input Output)].
Instance subG_historyΣ {Σ} `{Countable Eid} {Input Output : Type} :
subG (historyΣ Eid Input Output) Σ historyG Σ Eid Input Output.
Proof. solve_inG. Qed.
Section hist_own.
Context `{Countable Eid} {Input Output : Type} `{historyG Σ Eid Input Output}.
Notation vProp := (vProp Σ).
Notation event_map := (event_map Eid Input Output).
Notation event_set := (gset Eid).
Notation event_order := (gset (Eid * Eid)).
Notation EidO := (leibnizO Eid).
Notation eventO := (leibnizO (hist_event Input Output)).
Notation event_mapO := (gmap Eid eventO).
Notation event_setO := (gset EidO).
Implicit Types (events eventsM : event_map)
(owned ownedM : event_set)
(orders ordersM : event_order).
Definition AuthEvents γh eventsM ordersM : vProp :=
own γh (auth_events eventsM ordersM) .
Definition FragEvents γh f events owned orders : vProp :=
own γh (frag_events f events owned orders) .
Lemma Events_alloc γh f eid eV
eventsM events eventsM' events' owned owned' ordersM orders ordersM' orders'
(EVENTSM' : eventsM' = <[eid := eV]> eventsM)
(EVENTS' : events' = <[eid := eV]> events)
(ORDERSM' : ordersM' = new_orders (dom _ events) eid ordersM)
(ORDERS' : orders' = new_orders (dom _ events) eid orders)
(OWNED' : owned' = {[eid]} owned)
(FRESH : eventsM !! eid = None) :
AuthEvents γh eventsM ordersM - FragEvents γh f events owned orders
== AuthEvents γh eventsM' ordersM' FragEvents γh f events' owned' orders'.
Proof.
iIntros "Auth Frag".
iMod (own_update_2 _ _ _
((auth_events eventsM' ordersM') (frag_events f events' owned' orders'))
with "Auth Frag") as "[$ $]"; last done.
subst events' eventsM' owned' orders' ordersM'.
rewrite /auth_events /frag_events /wrap_events /to_agreeM !fmap_insert.
apply prod_update; simpl. apply prod_update; simpl.
- apply frac_auth_update, (alloc_local_update (A:= agreeR (leibnizO _))); [|done].
by rewrite lookup_fmap fmap_None.
- rewrite dom_insert_L. apply frac_auth_update, gset_disj_alloc_local_update.
assert (eid dom event_set eventsM) by by apply not_elem_of_dom.
set_solver.
- rewrite -!gset_op. by apply frac_auth_update, op_local_update_discrete.
Qed.
Lemma FragEvents_valid_2 γh f1 f2 events1 events2 owned1 owned2 orders1 orders2 :
FragEvents γh f1 events1 owned1 orders1
- FragEvents γh f2 events2 owned2 orders2
- (wrap_events events1 wrap_events events2)
owned1 ## owned2 .
Proof.
iIntros "Frag1 Frag2". iCombine "Frag1 Frag2" as "Frag".
iDestruct (own_valid with "Frag") as %VALID.
by move: VALID => /pair_valid [/pair_valid] [/frac_auth_frag_valid] [_ ?]
/frac_auth_frag_valid [_] /gset_disj_valid_op ?.
Qed.
Lemma FragEvents_split γh f1 f2 events1 events2 owned1 owned2 orders1 orders2
(AGREE : (wrap_events events1 wrap_events events2))
(DISJ : owned1 ## owned2) :
FragEvents γh (f1 + f2) (events1 events2) (owned1 owned2) (orders1 orders2)
(FragEvents γh f1 events1 owned1 orders1 FragEvents γh f2 events2 owned2 orders2)%I.
Proof.
rewrite -embed_sep -own_op. apply embed_proper, own_proper.
apply pair_proper; simpl. apply pair_proper; simpl.
- rewrite -frac_auth_frag_op. f_equiv. by rewrite event_map_op_join.
- rewrite -frac_auth_frag_op. rewrite gset_disj_union; [done|set_solver].
- rewrite -frac_auth_frag_op gset_op //.
Qed.
Lemma FragEvents_fork γh f1 f2 events owned1 owned2 orders (DISJ : owned1 ## owned2) :
FragEvents γh (f1 + f2) events (owned1 owned2) orders
- FragEvents γh f1 events owned1 orders FragEvents γh f2 events owned2 orders.
Proof.
iIntros "Frag".
have U1 : events events = events by apply map_self_id.
have U2 : orders orders = orders by set_solver.
rewrite -FragEvents_split; [by rewrite -{1}U1 -{1}U2|..|done].
move=> eid. rewrite /wrap_events lookup_op !lookup_fmap.
case E: (events !! eid) => [e|].
- rewrite !Some_valid. by apply (to_agree_op_valid_L (A:=eventO)).
- by rewrite /= op_None_left_id.
Qed.
Lemma FragEvents_join γh f1 f2 events1 events2 owned1 owned2 orders1 orders2 :
FragEvents γh f1 events1 owned1 orders1
- FragEvents γh f2 events2 owned2 orders2
- FragEvents γh (f1 + f2) (events1 events2) (owned1 owned2) (orders1 orders2).
Proof.
iIntros "Frag1 Frag2".
iDestruct (FragEvents_valid_2 with "Frag1 Frag2") as %[??].
iCombine "Frag1 Frag2" as "Frag".
rewrite event_map_op_join // gset_disj_union //.
Qed.
Lemma Events_included γh f eventsM events owned ordersM orders :
AuthEvents γh eventsM ordersM - FragEvents γh f events owned orders
- events eventsM orders ordersM .
Proof.
iIntros "oM oS". iDestruct (own_valid_2 with "oM oS") as %VALID.
iPureIntro. move: VALID => /pair_valid [/pair_valid] /= [VALIDE _] VALIDO.
move: VALIDE => /frac_auth_included_total
/(to_agreeM_included (A:=hist_event _ _)).
move: VALIDO => /frac_auth_included_total /gset_included. done.
Qed.
Lemma Events_full γh eventsM events owned ordersM orders :
AuthEvents γh eventsM ordersM - FragEvents γh 1 events owned orders
- events = eventsM orders = ordersM .
Proof.
iIntros "oM oS". iDestruct (own_valid_2 with "oM oS") as %VALID.
iPureIntro. move: VALID => /pair_valid [/pair_valid] /= [VALIDE _] VALIDO.
move: VALIDE => /frac_auth_agree
/(to_agreeM_agree (A:=hist_event _ _)).
move: VALIDO => /frac_auth_agree VALIDO. apply leibniz_equiv in VALIDO. done.
Qed.
End hist_own.
Require Import gpfsl.examples.sflib.
Require Import stdpp.namespaces.
From iris.algebra Require Import frac_auth gset gmap.
From gpfsl.lang Require Import notation.
From gpfsl.base_logic Require Import vprop.
From gpfsl.logic Require Import invariants proofmode.
From gpfsl.examples Require Import list_helper.
From gpfsl.examples.graph Require Import graph map_helper.
Set Default Proof Using "Type*".
Set Suggest Proof Using.
Section hist_event.
Context {Input Output : Type}.
(* Like [graph_event], but without [logview] (for encoding `hb`) since we only
consider linearizable DS operations *)
Record hist_event :=
mkHistEvent {
he_input : Input;
he_output : Output;
he_Vi : view;
he_Vo : view;
}.
#[global] Instance hist_event_inhab `{!Inhabited Input, !Inhabited Output} : Inhabited hist_event :=
populate (mkHistEvent inhabitant inhabitant inhabitant inhabitant).
End hist_event.
Arguments hist_event : clear implicits.
Notation event_map Eid Input Output := (gmap Eid (hist_event Input Output)).
Notation event_order Eid := (gset (Eid * Eid)).
Section event_list.
Context `{Countable Eid} {Input Output : Type}.
Notation hist_event := (hist_event Input Output).
Notation event_map := (event_map Eid Input Output).
Notation event_set := (gset Eid).
Notation event_order := (event_order Eid).
Implicit Types (events : event_map) (eid : Eid) (e : hist_event) (hs : list hist_event)
(orders : gset (Eid * Eid)) (eids : list Eid).
Definition event_list events eids hs :=
Forall2 (λ eid e, events !! eid = Some e) eids hs.
Definition eids_complete events eids := dom_list events eids.
Definition linearization orders eids :=
(i1 i2 : nat) (eid1 eid2 : Eid)
(EID1 : eids !! i1 = Some eid1)
(EID2 : eids !! i2 = Some eid2)
(ORDER : (eid1, eid2) orders),
(i1 < i2)%nat.
Definition sequential orders eids :=
(i1 i2 : nat) (eid1 eid2 : Eid)
(EID1 : eids !! i1 = Some eid1)
(EID2 : eids !! i2 = Some eid2)
(SEQ : (i1 < i2)%nat),
(eid1, eid2) orders.
Definition view_ordered events eid1 eid2 :=
e1 e2,
(events !! eid1) = Some e1
(events !! eid2) = Some e2
e1.(he_Vo) e2.(he_Vi).
Definition orders_consistent events orders :=
set_Forall (λ '(eid1, eid2), view_ordered events eid1 eid2) orders.
Definition new_orders (before : gset Eid) eid : event_order :=
set_map (λ eid', (eid', eid)) before.
End event_list.
Section hist_interpretation.
(* [Input]: command, [AObj]: abstract object, [init]: abstract object's initial
value, [run e o o']: adding an event [e] alters the object [o] into [o']. *)
Context `{Countable Eid} {Input Output AObj : Type}
(* TODO: change order of init and run *)
(init : AObj) (run : hist_event Input Output -> AObj -> AObj -> Prop).
Notation hist_event := (hist_event Input Output).
Notation event_map := (event_map Eid Input Output).
Notation event_set := (gset Eid).
Notation event_order := (event_order Eid).
Notation eids_of events := (dom event_set events).
Implicit Types (eid : Eid) (e : hist_event).
Inductive interp_history : (hs : list hist_event) (obj : AObj), Prop :=
| interp_history_nil : interp_history [] init
| interp_history_snoc {hs hs' obj obj' e}
(INTERP : interp_history hs obj)
(HIST' : hs' = hs ++ [e])
(RUN : run e obj obj')
: interp_history hs' obj'.
Lemma interp_history_invert_nil obj (INTERP : interp_history [] obj) : obj = init.
Proof. inversion INTERP; [done|subst]. by apply app_cons_not_nil in HIST'. Qed.
Lemma interp_history_invert_snoc hs hs' obj' e
(INTERP : interp_history hs' obj')
(HIST' : hs' = hs ++ [e])
: obj, interp_history hs obj run e obj obj'.
Proof.
inversion INTERP as [EMP|]; simplify_eq.
{ by apply app_cons_not_nil in EMP. }
apply app_inj_tail in HIST'0 as [<- <-].
by exists obj.
Qed.
End hist_interpretation.
Section sync.
Context {Σ : gFunctors}.
Context `{Countable Eid} {Input Output AObj : Type}.
Notation iProp := (iProp Σ).
Notation vProp := (vProp Σ).
Notation hist_event := (hist_event Input Output).
Notation event_map := (event_map Eid Input Output).
Notation event_set := (gset Eid).
Notation event_order := (event_order Eid).
Notation eids_of events := (dom event_set events).
Implicit Types (eid : Eid) (e : hist_event) (events : event_map) (V : view).
Definition seen_events events V : Prop :=
map_Forall (λ eid e, e.(he_Vo) V) events.
Lemma seen_events_events_flip_mono events1 events2 V :
events2 events1 seen_events events1 V seen_events events2 V.
Proof. move => ? SE ???. by eapply SE, lookup_weaken. Qed.