Timings for urpc_proof.v
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-perennial.dev/./src/program_proof/grove_shared/urpc_proof.v.timing
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-perennial.dev/./src/program_proof/grove_shared/urpc_proof.v.timing
From Perennial.Helpers Require Import ModArith.
From Goose.github_com.mit_pdos.gokv Require Import urpc.
From iris.algebra Require Import gset.
From iris.base_logic.lib Require Import saved_prop.
From Perennial.program_proof Require Import grove_prelude std_proof.
From Perennial.program_proof Require Import marshal_stateless_proof.
From Perennial.algebra Require Import auth_map.
From Perennial.base_logic Require Import lib.ghost_map lib.mono_nat lib.saved_spec.
From Perennial.goose_lang.lib Require Import slice.typed_slice.
(** Request descriptor: data describing a particular request *)
Record urpc_req_desc := ReqDesc {
urpc_reg_rpcid : u64;
urpc_reg_args : list u8;
urpc_reg_saved : gname; (* Saved pred storing what the reply needs to satisfy *)
urpc_reg_done : loc;
urpc_reg_rep_ptr : loc;
}.
Class urpcregG (Σ : gFunctors) := URpcRegG {
urpcreg_mono_natG :> mono_natG Σ;
urpcreg_mapG :> mapG Σ u64 urpc_req_desc;
urpcreg_escrowG :> mapG Σ u64 unit;
urpcreg_saved_gname_mapG :> mapG Σ u64 gname;
urpcreg_saved_urpc_specG :> savedSpecG Σ (list u8) (list u8);
urpcreg_savedG :> savedPredG Σ (list u8);
urpcreg_domG :> inG Σ (agreeR (gsetO u64));
}.
Definition urpcregΣ :=
#[mono_natΣ; mapΣ u64 urpc_req_desc; mapΣ u64 unit; mapΣ u64 gname; savedSpecΣ (list u8) (list u8); savedPredΣ (list u8);
GFunctor (agreeR (gsetO u64))].
Global Instance subG_urpcregG {Σ} :
subG urpcregΣ Σ → urpcregG Σ.
Section urpc_global_defs.
Context `{HPRE: !gooseGlobalGS Σ}.
(* A host-specific mapping from rpc ids on that host to pre/post conditions *)
Definition urpc_serverN : namespace := nroot.@"urpc_server".
Definition urpc_clientN : namespace := nroot.@"urpc_client".
Definition urpc_lockN : namespace := nroot.@"urpc_lock".
Definition urpc_escrowN : namespace := nroot.@"urpc_escrow".
Record client_chan_gnames := {
ccmapping_name : gname;
ccescrow_name : gname;
ccextracted_name : gname;
}.
Record server_chan_gnames := {
scmap_name : gname;
scset_name : gname;
}.
Definition reply_chan_inner_msg (Γ : client_chan_gnames) m : iProp Σ :=
∃ (rpcid seqno : u64) reqData replyData Post γ d rep,
"%Hlen_reply" ∷ ⌜ length replyData = int.nat (length replyData) ⌝ ∗
"%Henc" ∷ ⌜ msg_data m = u64_le seqno ++ replyData ⌝ ∗
"#Hseqno" ∷ ptsto_ro (ccmapping_name Γ) seqno (ReqDesc rpcid reqData γ d rep) ∗
"#HPost_saved" ∷ saved_pred_own γ DfracDiscarded (Post) ∗
"#HPost" ∷ inv urpc_escrowN (Post replyData ∨ ptsto_mut (ccescrow_name Γ) seqno 1 tt).
Definition reply_chan_inner (Γ : client_chan_gnames) (c: chan) : iProp Σ :=
∃ ms, "Hchan" ∷ c c↦ ms ∗
"Hmessages" ∷ [∗ set] m ∈ ms, reply_chan_inner_msg Γ m.
Implicit Type Spec : savedSpecO Σ (list u8) (list u8).
(* Crucially, this is persistent: note the □Spec *)
Definition server_chan_inner_msg Γsrv m : iProp Σ :=
∃ rpcid seqno args Spec Post Γ γ1 γ2 d rep rpcdom,
"%Hlen_args" ∷ ⌜ length args = int.nat (U64 (Z.of_nat (length args))) ⌝ ∗
"#Hdom1" ∷ own (scset_name Γsrv) (to_agree (rpcdom)) ∗
"%Hdom2" ∷ ⌜ rpcid ∈ rpcdom ⌝ ∗
"%Henc" ∷ ⌜ msg_data m = u64_le rpcid ++ u64_le seqno ++ args ⌝ ∗
"#Hseqno" ∷ ptsto_ro (ccmapping_name Γ) seqno (ReqDesc rpcid args γ1 d rep) ∗
"#Hspec_name" ∷ ptsto_ro (scmap_name Γsrv) rpcid γ2 ∗
"#Hspec_saved" ∷ saved_spec_own γ2 Spec ∗
"#HPre" ∷ □ Spec args Post ∗
"#HPost_saved" ∷ saved_pred_own γ1 DfracDiscarded (Post) ∗
"#Hclient_chan_inv" ∷ inv urpc_clientN (reply_chan_inner Γ (msg_sender m)).
Definition server_chan_inner (c: chan) γmap : iProp Σ :=
∃ ms,
"Hchan" ∷ c c↦ ms ∗
"Hmessages" ∷ [∗ set] m ∈ ms, server_chan_inner_msg γmap m.
(** The given [rpcid] on the given [host] has the given [Spec], where [Spec] is
a predicate-transformer (similar to WP). *)
Definition is_urpc_spec_pred Γsrv (host:chan) (rpcid:u64) Spec : iProp Σ :=
(∃ γ rpcdom,
"#Hdom1" ∷ own (scset_name Γsrv) (to_agree (rpcdom)) ∗
"%Hdom2" ∷ ⌜ rpcid ∈ rpcdom ⌝ ∗
"#Hspec_name" ∷ ptsto_ro (scmap_name Γsrv) rpcid γ ∗
"#Hspec_saved" ∷ saved_spec_own γ Spec ∗
"#Hserver_inv" ∷ inv urpc_serverN (server_chan_inner host Γsrv)
)%I.
Global Instance is_urpc_spec_pred_pers γ host rpcid Spec :
Persistent (is_urpc_spec_pred γ host rpcid Spec).
Global Instance is_urpc_spec_pred_contractive γ host rpcid :
Contractive (is_urpc_spec_pred γ host rpcid).
Definition is_urpc_dom Γsrv (d: gset u64) :=
own (scset_name Γsrv) (to_agree d).
Context `{hG: !heapGS Σ}.
Context `{hReg: !urpcregG Σ}.
(** This function [f] implements the given handler spec. *)
Definition is_urpc_handler_pred (f:val)
(Spec : list u8 → (list u8 → iProp Σ) → iProp Σ)
: iProp Σ :=
∀ (reqData:list u8) Post req rep,
{{{
own_slice_small req byteT 1 reqData ∗
rep ↦[slice.T byteT] (slice_val Slice.nil) ∗
Spec reqData Post
}}}
f (slice_val req) #rep
{{{ rep_sl q repData, RET #();
rep ↦[slice.T byteT] (slice_val rep_sl) ∗
own_slice_small rep_sl byteT q repData ∗
Post repData
}}}.
Definition Client_lock_inner Γ (cl : loc) (lk : loc) mref : iProp Σ :=
∃ pending reqs (estoks extoks : gmap u64 unit) (n : u64),
"%Hnpos" ∷ ⌜ 0 < int.Z n ⌝%Z ∗
"%Hdom_range" ∷ ⌜ ∀ id, (0 < int.Z id < int.Z n)%Z ↔ id ∈ dom reqs ⌝ ∗
"%Hdom_eq_es" ∷ ⌜ dom reqs = dom estoks ⌝ ∗
"%Hdom_eq_ex" ∷ ⌜ dom reqs = dom extoks ⌝ ∗
"%Hdom_pending" ∷ ⌜ dom pending ⊆ dom reqs ⌝ ∗
"seq" ∷ cl ↦[Client :: "seq"] #n ∗
"Hmapping_ctx" ∷ map_ctx (ccmapping_name Γ) 1 reqs ∗
"Hescrow_ctx" ∷ map_ctx (ccescrow_name Γ) 1 estoks ∗
"Hextracted_ctx" ∷ map_ctx (ccextracted_name Γ) 1 extoks ∗
"Hpending_map" ∷ map.own_map mref 1 (pending, zero_val ptrT) ∗
"Hreqs" ∷ [∗ map] seqno ↦ req ∈ reqs,
∃ (Post : list u8 → iProp Σ),
"Hreg_entry" ∷ ptsto_ro (ccmapping_name Γ) seqno req ∗
"HPost_saved" ∷ saved_pred_own (urpc_reg_saved req) DfracDiscarded (Post) ∗
(* (1) Reply thread has not yet processed, so it is in pending
and we have escrow token *)
((∃ (cb : loc) (cb_cond : loc) dummy (aborted : bool),
"%Hpending_cb" ∷ ⌜ pending !! seqno = Some #cb ⌝ ∗
"#reply" ∷ readonly (cb ↦[Callback :: "reply"] #(urpc_reg_rep_ptr req)) ∗
"#state" ∷ readonly (cb ↦[Callback :: "state"] #(urpc_reg_done req)) ∗
"#cond" ∷ readonly (cb ↦[Callback :: "cond"] #cb_cond) ∗
"Hescrow" ∷ ptsto_mut (ccescrow_name Γ) seqno 1 tt ∗
"#Hcond" ∷ is_cond cb_cond #lk ∗
"Hrep_ptr" ∷ (urpc_reg_rep_ptr req) ↦[slice.T byteT] dummy ∗
"Hstate" ∷ (urpc_reg_done req) ↦[uint64T] #(LitInt $ if aborted then 2 else 0)) ∨
(* (2) Reply thread has received message, removed from pending,
but caller has not extracted ownership *)
(∃ reply rep_sl,
"%Hpending_cb" ∷ ⌜ pending !! seqno = None ⌝ ∗
"HPost" ∷ (Post reply) ∗
"Hrep_ptr" ∷ (urpc_reg_rep_ptr req) ↦[slice.T byteT] (slice_val rep_sl) ∗
"Hrep_data" ∷ own_slice_small rep_sl byteT 1 reply ∗
"Hstate" ∷ (urpc_reg_done req) ↦[uint64T] #1) ∨
(* (3) Caller has extracted ownership *)
(⌜ pending !! seqno = None ⌝ ∗ ptsto_mut (ccextracted_name Γ) seqno 1 tt)).
Definition is_uRPCClient (cl : loc) (srv : chan) : iProp Σ :=
∃ Γ (lk : loc) client (mref : loc),
"#Hstfields" ∷ ("mu" ∷ readonly (cl ↦[Client :: "mu"] #lk) ∗
"#conn" ∷ readonly (cl ↦[Client :: "conn"] connection_socket client srv) ∗
"#pending" ∷ readonly (cl ↦[Client :: "pending"] #mref)) ∗
"#Hchan" ∷ inv urpc_clientN (reply_chan_inner Γ client) ∗
"#Hlk" ∷ is_lock urpc_lockN #lk (Client_lock_inner Γ cl lk mref).
Definition Client_reply_own (cl : loc) : iProp Σ :=
∃ Γ (lk : loc) client srv (mref : loc),
"#Hstfields" ∷ ("mu" ∷ readonly (cl ↦[Client :: "mu"] #lk) ∗
"#conn" ∷ readonly (cl ↦[Client :: "conn"] connection_socket client srv) ∗
"#pending" ∷ readonly (cl ↦[Client :: "pending"] #mref)) ∗
"#Hchan" ∷ inv urpc_clientN (reply_chan_inner Γ client) ∗
"#Hlk" ∷ is_lock urpc_lockN #lk (Client_lock_inner Γ cl lk mref).
Global Instance own_map_AsMapsTo mref (hd:gmap u64 val * val) :
AsMapsTo (map.own_map mref 1 hd) (λ q, map.own_map mref q hd).
split; try apply _; eauto.
rewrite /fractional.Fractional.
iDestruct 1 as (mv Heq) "H".
iDestruct "H" as "(H1&H2)".
iSplitL "H1"; iExists _; iFrame; eauto.
iDestruct "H1" as (hd1 Heq) "H1".
iDestruct "H2" as (hd2 Heq') "H2".
iDestruct (heap_mapsto_agree with "[$H1 $H2]") as %Heq''.
iExists _; iSplit; first done.
Definition own_Server (s : loc) (handlers: gmap u64 val) : iProp Σ :=
∃ mref def,
"#Hhandlers_map" ∷ readonly (map.own_map mref 1 (handlers, def)) ∗
"#handlers" ∷ readonly (s ↦[Server :: "handlers"] #mref).
Lemma wp_MakeServer (handlers : gmap u64 val) (mref:loc) (def : val) :
{{{
map.own_map mref 1 (handlers, def)
}}}
MakeServer #mref @ ⊤
{{{
(s:loc), RET #s; own_Server s handlers
}}}.
wp_apply (wp_allocStruct); first val_ty.
iDestruct (struct_fields_split with "Hs") as "Hs".
unshelve (iMod (readonly_alloc_1 with "handlers") as "#handlers"); [| apply _ |].
unshelve (iMod (readonly_alloc_1 with "Hmap") as "#Hmap"); [| apply _ |].
Definition urpc_handler_mapping (γ : server_chan_gnames) (host : u64) (handlers : gmap u64 val) : iProp Σ :=
([∗ map] rpcid↦handler ∈ handlers, ∃ Spec,
is_urpc_spec_pred γ host rpcid Spec ∗
is_urpc_handler_pred handler Spec)%I.
Lemma non_empty_urpc_handler_mapping_inv γ host handlers :
dom handlers ≠ ∅ →
urpc_handler_mapping γ host handlers -∗
"#Hserver_inv" ∷ inv urpc_serverN (server_chan_inner host γ) ∗
"#Hhandlers" ∷ ([∗ map] rpcid↦handler ∈ handlers, ∃ Spec γs,
ptsto_ro (scmap_name γ) rpcid γs ∗
saved_spec_own γs Spec ∗
is_urpc_handler_pred handler Spec)%I.
iIntros (Hdom) "Hmapping".
iInduction handlers as [| rpcid handler] "IH" using map_ind.
rewrite dom_empty_L in Hdom; congruence.
rewrite /urpc_handler_mapping big_sepM_insert //.
iDestruct "Hmapping" as "(H&Hmapping)".
destruct (decide (dom m = ∅)) as [Hemp|Hemp].
iDestruct "H" as "(His_urpc_spec_pred&His_urpcHandler)".
iNamed "His_urpc_spec_pred".
rewrite big_sepM_insert //.
iSplitL "His_urpcHandler".
apply dom_empty_iff_L in Hemp.
rewrite Hemp big_sepM_empty.
iDestruct ("IH" with "[//] [$]") as "HIH".
rewrite big_sepM_insert //.
iDestruct "H" as "(His_urpc_spec_pred&His_urpcHandler)".
rewrite /is_urpc_spec_pred.
iDestruct "His_urpc_spec_pred" as (g0 rpcdom) "H".
iDestruct "H" as "(#Hdom1&%Hdom2&#Hspec_name&#Hspec_saved&H)".
Definition handlers_complete Γ (handlers : gmap u64 val) :=
(is_urpc_dom Γ (dom handlers)).
Lemma wp_Server__readThread γ s host client handlers mref def :
dom handlers ≠ ∅ →
"#Hcomplete" ∷ handlers_complete γ handlers ∗
"#His_rpc_map" ∷ urpc_handler_mapping γ host handlers ∗
"#Hhandlers_map" ∷ readonly (map.own_map mref 1 (handlers, def)) ∗
"#handlers" ∷ readonly (s ↦[Server :: "handlers"] #mref) -∗
WP Server__readThread #s (connection_socket host client) {{ _, True }}.
wp_apply (wp_forBreak_cond'); [ iNamedAccu |].
iDestruct (non_empty_urpc_handler_mapping_inv with "[$]") as "H"; first auto.
iInv "Hserver_inv" as "Hchan_inner" "Hclo".
iDestruct "Hchan_inner" as (ms) "(>Hchan'&#Hchan_inner)".
iApply (ncfupd_mask_intro _); first set_solver+.
iIntros (err m) "(Hchan&Herr)".
iAssert (if err then True else ▷ server_chan_inner_msg γ (Message client m))%I with "[Hchan_inner Herr]" as "Hmsg".
iDestruct "Herr" as %Hin.
iApply (big_sepS_elem_of with "Hchan_inner"); first eassumption.
iMod ("Hclo" with "[Hchan]") as "_".
iDestruct (own_slice_to_small with "Hsl") as "Hsl".
wp_apply (wp_ReadInt with "Hsl").
wp_apply (wp_ReadInt with "Hsl").
wp_apply (wp_fork with "[-]"); last first.
wp_apply (wp_ref_of_zero); first done.
iMod (readonly_load with "Hhandlers_map") as (?) "Hmap_read".
wp_apply (map.wp_MapGet with "[$]").
iIntros (v ok) "(%Hget&_)".
rewrite /map.map_get in Hget.
destruct (handlers !! rpcid) as [f|] eqn:Hlookup'; last first.
iDestruct (own_valid_2 with "Hcomplete Hdom1") as %Hval.
apply to_agree_op_inv_L in Hval.
apply not_elem_of_dom in Hlookup'.
iDestruct (big_sepM_lookup with "Hhandlers") as "H"; eauto.
iDestruct "H" as "(#Hsname&#Hsaved&#His_urpcHandler)".
iDestruct (ptsto_ro_agree with "Hspec_name Hsname") as %->.
iDestruct (saved_spec_agree _ _ _ args Post with "Hspec_saved Hsaved")
as "#Hequiv".
rewrite /is_urpc_handler_pred.
wp_apply ("His_urpcHandler" with "[$Hsl $Hsl']").
iIntros (rep_sl rep_q repData) "(Hsl' & Hown_slice & HPost)".
iDestruct (own_slice_small_sz with "Hown_slice") as %Hsz.
wp_apply (wp_LoadAt with "[$]").
wp_apply (wp_NewSliceWithCap (V:=u8)).
apply encoding.unsigned_64_nonneg.
(* FIXME why does [word] not solve this? *)
wp_apply (wp_WriteInt with "Hmsg").
wp_apply (wp_WriteBytes with "[$Hmsg $Hown_slice]").
iIntros (msg_sl) "[Hmsg_slice _]".
rewrite -!app_assoc app_nil_l.
iDestruct (own_slice_small_read with "Hmsg_slice") as "(Hmsg_slice&_)".
wp_apply (wp_Send with "[$Hmsg_slice]").
iMod (inv_alloc urpc_escrowN _ (Post repData ∨ ptsto_mut (ccescrow_name Γ) seqno 1 tt)
with "[HPost]") as "#HPost_escrow".
iInv "Hclient_chan_inv" as "Hclient_chan_inner" "Hclo".
iDestruct "Hclient_chan_inner" as (ms_rep) "(>Hchan'&#Hclient_chan_inner)".
iApply (ncfupd_mask_intro _); first set_solver+.
iIntros (msg_sent) "Hchan'".
iMod ("Hclo" with "[Hchan']").
destruct msg_sent; last first.
iEval (rewrite [ms_rep ∪ _]comm_L).
iApply big_sepS_insert_2; last done.
iExists _, _, _, _, _, _, _, _.
Lemma wp_StartServer_pred γ (host : u64) (handlers : gmap u64 val) (s : loc) :
dom handlers ≠ ∅ →
{{{
handlers_complete γ handlers ∗
own_Server s handlers ∗
[∗ map] rpcid ↦ handler ∈ handlers,
(∃ Spec, is_urpc_spec_pred γ host rpcid Spec ∗ is_urpc_handler_pred handler Spec)
}}}
Server__Serve #s #host
{{{
RET #(); True
}}}.
iIntros (? Φ) "(#Hcomplete&Hserver&#His_rpc_map) HΦ".
wp_apply (wp_forBreak_cond'); [ iNamedAccu |].
wp_apply (wp_Server__readThread with "[]"); eauto.
Lemma wp_Client__replyThread cl :
Client_reply_own cl -∗
WP Client__replyThread #cl {{ _, True }}.
wp_apply (wp_forBreak' True%I with "[-]").
iInv "Hchan" as "Hchan_inner" "Hclo".
iDestruct "Hchan_inner" as (ms) "(>Hchan'&#Hchan_inner)".
iApply (ncfupd_mask_intro _); first set_solver+.
iIntros (err m) "(Hchan'&Herr)".
iAssert (if err then True else ▷ reply_chan_inner_msg Γ (Message srv m))%I with "[Hchan_inner Herr]" as "Hmsg".
iDestruct "Herr" as %Hin.
iApply (big_sepS_elem_of with "Hchan_inner"); first eassumption.
iMod ("Hclo" with "[Hchan']") as "_".
(* Loop (MapIter) to wake up all waiting clients *)
wp_apply (acquire_spec with "[$]").
iIntros "(Hlked&Hlock_inner)".
wp_apply (map.wp_MapIter with "Hpending_map Hreqs").
instantiate (1:=λ k v, ⌜pending !! k = Some v⌝%I).
iIntros (k v Φ) "!# [Hreqs %Hm] HΦ".
(* First step to strip ▷, then freeze. *)
assert (is_Some (reqs !! k)) as [req Hreq].
apply elem_of_dom, Hdom_pending, elem_of_dom.
iDestruct (big_sepM_lookup_acc _ _ k req with "Hreqs") as "[Hreq Hreqs]"; first done.
iDestruct "Hreq" as "[Hreq|[Hreq|[% _]]]"; last first.
by destruct (pending !! k).
by destruct (pending !! k).
rewrite Hpending_cb in Hm.
wp_apply (wp_condSignal with "Hcond").
iDestruct ("Hreqs" with "[-HΦ]") as "Hreqs".
iFrame "Hreg_entry HPost_saved".
instantiate (1:=λ k v, ⌜True⌝%I).
iIntros "[Hmap [Hreqs _]]".
wp_apply (release_spec with "[-]").
iDestruct (typed_slice.own_slice_to_small with "Hs") as "Hsl".
wp_apply (wp_ReadInt with "Hsl").
wp_apply (acquire_spec with "[$]").
iIntros "(Hlked&Hlock_inner)".
wp_apply (map.wp_MapGet with "[$]").
iIntros (v ok) "(%Hget&Hpending_map)".
wp_if_destruct; last first.
wp_apply (release_spec with "[-]").
wp_apply (map.wp_MapDelete with "[$]").
iDestruct (map_ro_valid with "Hmapping_ctx [$]") as %Hlookup_reg.
iDestruct (big_sepM_delete with "Hreqs") as "(H&Hclo)"; first eauto.
iRename "HPost_saved" into "Hsaved".
iDestruct "H" as "[Hcase1|[Hcase2|Hcase3]]".
apply map.map_get_true in Hget.
rewrite Hget in Hpending_cb.
inversion Hpending_cb as [Heq].
wp_apply (wp_StoreAt with "[Hrep_ptr]").
wp_apply (wp_StoreAt with "[Hstate]").
wp_apply (wp_condSignal with "[$]").
iInv "HPost" as "HPost_inner" "Hclo''".
iDestruct "HPost_inner" as "[HPost_val|>Hescrow']"; last first.
iDestruct (ptsto_valid_2 with "Hescrow [$]") as %Hval.
iMod ("Hclo''" with "[Hescrow]").
wp_apply (release_spec with "[-]"); last first.
iExists (delete seqno pending) , _, _, _, _.
iApply big_sepM_delete; first eassumption.
iSplitR "Hclo"; last first.
iApply (big_sepM_mono with "Hclo").
iIntros (?? Hlookup) "H".
iFrame "Hreg_entry HPost_saved".
iDestruct "H" as "[Hcase1|[Hcase2|Hcase3]]".
iExists _, _, _, aborted0.
destruct (decide (seqno = k)).
rewrite lookup_delete in Hlookup; congruence.
rewrite lookup_delete_ne //=.
apply lookup_delete_None; auto.
iDestruct "Hcase3" as "(%&H)".
apply lookup_delete_None; auto.
apply lookup_delete_None; auto.
iDestruct "Hcase2" as "(%Hlookup&_)".
apply map.map_get_true in Hget.
iDestruct "Hcase3" as "(%Hlookup&_)".
apply map.map_get_true in Hget.
Lemma wp_TryMakeClient (srv:u64):
{{{
True
}}}
TryMakeClient #srv
{{{
(err:u64) (cl_ptr:loc), RET (#err, #cl_ptr);
if (decide (err = 0)) then
is_uRPCClient cl_ptr srv
else
True
}}}.
iIntros (err client) "Hr".
wp_apply (wp_ref_of_zero).
wp_apply (wp_new_free_lock).
wp_apply (map.wp_NewMap).
wp_apply (wp_allocStruct); first val_ty.
iDestruct (struct_fields_split with "Hcl") as "Hcl".
(* TODO: why do I have to unshelve this, when in other cases it appears to get picked up automatically *)
unshelve (iMod (readonly_alloc_1 with "mu") as "#mu"); [| apply _ |].
unshelve (iMod (readonly_alloc_1 with "conn") as "#conn"); [| apply _ |].
unshelve (iMod (readonly_alloc_1 with "pending") as "#pending"); [| apply _ |].
iMod (map_init (∅ : gmap u64 urpc_req_desc)) as (γccmapping) "Hmapping_ctx".
iMod (map_init (∅ : gmap u64 unit)) as (γccescrow) "Hescrow_ctx".
iMod (map_init (∅ : gmap u64 unit)) as (γccextracted) "Hextracted_ctx".
set (Γ := {| ccmapping_name := γccmapping; ccescrow_name := γccescrow;
ccextracted_name := γccextracted |}).
iMod (alloc_lock urpc_lockN _ _ (Client_lock_inner Γ cl lk mref) with
"Hfree [Hmapping_ctx Hescrow_ctx Hextracted_ctx seq Hmref]") as "#Hlock".
split; last by set_solver.
rewrite big_sepM_empty //.
iMod (inv_alloc urpc_clientN _ (reply_chan_inner Γ client) with "[Hr]") as "#Hchan_inv".
rewrite big_sepS_empty //.
iApply wp_Client__replyThread.
1:iFrame "mu conn pending".
iSplit; first by iFrame "#".
Lemma wp_MakeClient (srv:u64):
{{{
True
}}}
MakeClient #srv
{{{
(cl_ptr:loc), RET #cl_ptr; is_uRPCClient cl_ptr srv
}}}.
wp_apply (wp_TryMakeClient).
iIntros (err client) "Hr".
apply bool_decide_eq_true in Herr.
replace (err) with (U64 0) by naive_solver.
destruct (decide _); last first.
Inductive call_err := CallErrTimeout | CallErrDisconnect.
Definition call_errno (err : option call_err) : Z :=
match err with
| None => 0
| Some CallErrTimeout => 1
| Some CallErrDisconnect => 2
end.
Definition own_uRPC_Callback (cl_ptr cb_ptr : loc) Post : iProp Σ :=
∃ n Γ γ rpcid reqData cb_cond (rep_ptr cb_state lk mref : loc),
"#mu" ∷ readonly (cl_ptr ↦[Client :: "mu"] #lk) ∗
"#Hlk" ∷ is_lock urpc_lockN #lk (Client_lock_inner Γ cl_ptr lk mref) ∗
"#cond'" ∷ is_cond cb_cond #lk ∗
"#reply" ∷ readonly (cb_ptr ↦[Callback :: "reply"] #rep_ptr) ∗
"#state" ∷ readonly (cb_ptr ↦[Callback :: "state"] #cb_state) ∗
"#cond" ∷ readonly (cb_ptr ↦[Callback :: "cond"] #cb_cond) ∗
"#Hsaved" ∷ saved_pred_own γ DfracDiscarded Post ∗
"#Hreg" ∷ n [[Γ.(ccmapping_name)]]↦ro {|
urpc_reg_rpcid := rpcid;
urpc_reg_args := reqData;
urpc_reg_saved := γ;
urpc_reg_done := cb_state;
urpc_reg_rep_ptr := rep_ptr
|} ∗
"Hextracted" ∷ n [[Γ.(ccextracted_name)]]↦ ().
Lemma wp_Client__CallStart_pred γsmap (cl_ptr:loc) (rpcid:u64) (host:u64) req
(reqData:list u8) Spec Post q :
is_urpc_spec_pred γsmap host rpcid Spec -∗
{{{
own_slice_small req byteT q reqData ∗
is_uRPCClient cl_ptr host ∗
□(▷ Spec reqData Post)
}}}
Client__CallStart #cl_ptr #rpcid (slice_val req)
{{{
(err : option call_err) (cb_ptr : loc), RET (#cb_ptr, #(call_errno err));
own_slice_small req byteT q reqData ∗
(if err is Some _ then True else own_uRPC_Callback cl_ptr cb_ptr Post)
}}}.
iIntros "#Hhandler !#" (Φ) "H HΦ".
iDestruct "H" as "(Hslice&Hclient&#HSpec)".
wp_apply (wp_ref_of_zero).
iIntros (rep_ptr) "Hrep_ptr".
wp_apply (wp_ref_of_zero); first done.
iIntros (cb_state) "cb_state".
wp_bind (lock.newCond _).
wp_apply (wp_newCond with "[$]").
iIntros (cb_cond) "#cond".
wp_apply (wp_allocStruct); first val_ty.
iRename "cond" into "cond'".
iDestruct (struct_fields_split with "Hcb") as "Hcb".
unshelve (iMod (readonly_alloc_1 with "reply") as "#reply"); [| apply _ |].
unshelve (iMod (readonly_alloc_1 with "state") as "#state"); [| apply _ |].
unshelve (iMod (readonly_alloc_1 with "cond") as "#cond"); [| apply _ |].
wp_apply (wp_StoreAt with "[$]"); first eauto.
wp_apply (acquire_spec with "[$]").
iIntros "(Hlked&Hlock_inner)".
wp_apply wp_SumAssumeNoOverflow.
wp_apply (map.wp_MapInsert with "[$]").
iMod (saved_pred_alloc (Post)) as (γ) "#Hsaved".
apply dfrac_valid_discarded.
assert (reqs !! n = None).
iMod (map_alloc_ro n (ReqDesc rpcid reqData γ cb_state rep_ptr)
with "Hmapping_ctx") as "(Hmapping_ctx&#Hreg)"; auto.
iMod (map_alloc n tt with "Hescrow_ctx") as "(Hescrow_ctx&Hescrow)".
rewrite -Hdom_eq_es -Hdom_range.
iMod (map_alloc n tt with "Hextracted_ctx") as "(Hextracted_ctx&Hextracted)".
rewrite -Hdom_eq_ex -Hdom_range.
wp_apply (release_spec with "[-Hslice Hhandler HΦ Hextracted]").
replace (int.Z (word.add n 1)) with (int.Z n + 1)%Z by word.
assert (0 < int.Z id < int.Z n ∨ int.Z id = int.Z n)%Z.
iSplit; first (iPureIntro; congruence).
iSplit; first (iPureIntro; congruence).
iSplit; first (iPureIntro; set_solver).
rewrite big_sepM_insert; last first.
iSplitR "Hreqs"; last first.
iApply (big_sepM_mono with "Hreqs").
iIntros (k req' Hlookup).
iDestruct 1 as (Post') "H".
setoid_rewrite lookup_insert_ne; eauto.
rewrite lookup_insert //.
wp_apply (wp_NewSliceWithCap (V:=u8)).
apply encoding.unsigned_64_nonneg.
(* FIXME why does [word] not solve this? *)
wp_apply (wp_WriteInt with "Hmsg").
wp_apply (wp_WriteInt with "Hmsg").
wp_apply (wp_WriteBytes with "[$Hmsg $Hslice]").
iIntros (req_sl) "[Hreq_sl Hslice]".
rewrite -!app_assoc app_nil_l.
iDestruct (own_slice_to_small with "Hreq_sl") as "Hreq_sl".
wp_apply (wp_Send with "[$]").
iInv "Hserver_inv" as "Hserver_inner" "Hclo".
iDestruct "Hserver_inner" as (ms) "(>Hchan'&Hmessages)".
iApply (ncfupd_mask_intro _); first set_solver+.
iIntros (msg_sent) "Hchan'".
iDestruct (own_slice_small_sz with "Hslice") as %Hsz.
iMod ("Hclo" with "[Hmessages Hchan']") as "_".
destruct msg_sent; last by iFrame.
iApply (big_sepS_insert_2 with "[] Hmessages").
iExists _, _, _, _, _, _, _.
assert (U64 (Z.of_nat (int.nat (req.(Slice.sz)))) = req.(Slice.sz)) as Heqlen.
iIntros (err) "[%Herr _]".
wp_apply wp_allocStruct; first val_ty.
iApply ("HΦ" $! (Some CallErrDisconnect) cb_ptr).
iApply ("HΦ" $! None cb).
Lemma wp_Client__CallComplete_pred (cl_ptr cb_ptr:loc) rep_out_ptr
(timeout_ms : u64) dummy_sl_val Post :
{{{
rep_out_ptr ↦[slice.T byteT] dummy_sl_val ∗
own_uRPC_Callback cl_ptr cb_ptr Post
}}}
Client__CallComplete #cl_ptr #cb_ptr #rep_out_ptr #timeout_ms
{{{
(err : option call_err), RET #(call_errno err);
(if err is Some _ then rep_out_ptr ↦[slice.T byteT] dummy_sl_val else
∃ rep_sl (repData:list u8),
rep_out_ptr ↦[slice.T byteT] (slice_val rep_sl) ∗
own_slice_small rep_sl byteT 1 repData ∗
(Post repData))
}}}.
iIntros (Φ) "[Hrep_out_ptr Hcb] HΦ".
wp_apply (acquire_spec with "[$]").
wp_bind (if: _ then _ else _)%E.
iAssert (∃ (x: u64), cb_state ↦[uint64T] #x ∗ n [[Γ.(ccextracted_name)]]↦ () ∗
(cb_state ↦[uint64T] #x -∗ Client_lock_inner Γ cl_ptr lk mref))%I
with "[Hlockinv Hextracted]" as "H".
iDestruct (map_ro_valid with "Hmapping_ctx [$]") as %Hlookup_reg.
iDestruct (big_sepM_lookup_acc with "Hreqs") as "(H&Hclo)"; first eauto.
iDestruct "H" as "[Hcase1|[Hcase2|Hcase3]]".
iDestruct "Hcase1" as "(#?&#?&#?&Hrest)".
iFrame "HPost_saved Hreg".
iDestruct "Hcase3" as "(?&Hex)".
iDestruct (ptsto_valid_2 with "Hex [$]") as %Hval.
iDestruct "H" as (b) "(Hdone&Hextracted&Hdone_clo)".
wp_apply (wp_LoadAt with "[$]").
iDestruct ("Hdone_clo" with "[$]") as "Hlockinv".
wp_apply (wp_If_join_evar' (lock.locked #lk ∗
Client_lock_inner Γ cl_ptr lk mref)%I
with "[Hi Hlockinv]").
case_bool_decide; wp_pures.
wp_apply (wp_condWaitTimeout with "[$cond' $Hi $Hlk $Hlockinv]").
iDestruct (map_ro_valid with "Hmapping_ctx [$]") as %Hlookup_reg.
iDestruct (big_sepM_lookup_acc with "Hreqs") as "(H&Hclo)"; first eauto.
iDestruct "H" as "[Hcase1|[Hcase2|Hcase3]]".
iDestruct "Hcase1" as "(#?&#?&#?&Hrest)".
wp_apply (wp_LoadAt with "[$]").
iDestruct ("Hclo" with "[Hdone Hcond Hescrow Hrep_ptr]") as "H".
rewrite bool_decide_false.
wp_apply (release_spec with "[$Hlk $Hi H HPost_saved
Hpending_map Hmapping_ctx Hescrow_ctx Hextracted_ctx seq]").
destruct aborted; wp_pures; iModIntro.
1: iApply ("HΦ" $! (Some CallErrDisconnect)).
2: iApply ("HΦ" $! (Some CallErrTimeout)).
wp_apply (wp_LoadAt with "[$]").
iDestruct (saved_pred_agree _ _ _ _ _ reply with "HPost_saved Hsaved") as "#Hequiv".
wp_apply (wp_LoadAt with "[$Hrep_ptr]").
wp_apply (wp_StoreAt with "[$Hrep_out_ptr]").
iDestruct ("Hclo" with "[Hdone Hextracted]") as "H".
wp_apply (release_spec with "[$Hlk $Hi H HPost_saved
Hpending_map Hmapping_ctx Hescrow_ctx Hextracted_ctx seq]").
iRewrite ("Hequiv") in "HPost".
iDestruct "Hcase3" as "(?&Hex)".
iDestruct (ptsto_valid_2 with "Hex [$]") as %Hval.
Lemma wp_Client__Call_pred γsmap (cl_ptr:loc) (rpcid:u64) (host:u64) req rep_out_ptr
(timeout_ms : u64) dummy_sl_val (reqData:list u8) Spec Post q :
{{{
"Hslice" ∷ own_slice_small req byteT q reqData ∗
"Hrep_out_ptr" ∷ rep_out_ptr ↦[slice.T byteT] dummy_sl_val ∗
"#Hclient" ∷ is_uRPCClient cl_ptr host ∗
"#Hhandler" ∷ is_urpc_spec_pred γsmap host rpcid Spec ∗
"#HSpec" ∷ □(▷ Spec reqData Post)
}}}
Client__Call #cl_ptr #rpcid (slice_val req) #rep_out_ptr #timeout_ms
{{{
(err : option call_err), RET #(call_errno err);
own_slice_small req byteT q reqData ∗
(if err is Some _ then rep_out_ptr ↦[slice.T byteT] dummy_sl_val else
∃ rep_sl (repData:list u8),
rep_out_ptr ↦[slice.T byteT] (slice_val rep_sl) ∗
own_slice_small rep_sl byteT 1 repData ∗
(Post repData))
}}}.
wp_apply (wp_Client__CallStart_pred with "Hhandler [$Hslice $Hclient $HSpec]").
iIntros (err cb_ptr) "[Hslice Hcb]".
destruct err as [err|]; wp_pures.
2: iApply ("HΦ" $! (Some CallErrDisconnect)).
1: iApply ("HΦ" $! (Some CallErrTimeout)).
wp_apply (wp_Client__CallComplete_pred with "[$Hrep_out_ptr $Hcb]").
iIntros ([err|]) "Hcomplete".
iApply ("HΦ" $! (Some err)).
(** With this spec, there's no need to specify an "intermediate" postcondition,
but the Φ shows up in a magic wand under □, so you may need to use
wp_frame_wand in order to get resources (such as "HΦ") across the □. *)
Lemma wp_Client__Call2 γsmap (cl_ptr:loc) (rpcid:u64) (host:u64) req rep_out_ptr
(timeout_ms : u64) dummy_sl_val (reqData:list u8) Spec Φ q :
is_uRPCClient cl_ptr host -∗
is_urpc_spec_pred γsmap host rpcid Spec -∗
own_slice_small req byteT q reqData -∗
rep_out_ptr ↦[slice.T byteT] dummy_sl_val -∗
□(▷ Spec reqData (λ reply,
own_slice_small req byteT q reqData -∗
∀ rep_sl,
rep_out_ptr ↦[slice.T byteT] (slice_val rep_sl) -∗
own_slice_small rep_sl byteT 1 reply -∗
Φ #0)
) ∧
(
∀ (err:u64), ⌜err ≠ 0⌝ →
own_slice_small req byteT q reqData -∗
rep_out_ptr ↦[slice.T byteT] dummy_sl_val -∗ Φ #err
) -∗
WP Client__Call #cl_ptr #rpcid (slice_val req) #rep_out_ptr #timeout_ms {{ Φ }}.
iIntros "#His_cl #Hhandler Hreq_sl Hrep [#Hspec Hfail]".
wp_apply (wp_Client__Call_pred with "[Hhandler His_cl Hreq_sl Hrep]").
(* FIXME: iFrame "#" doesn't work without clearing the name. *)
iDestruct "Hpost" as "(Hreq&Hrep)".
iApply ("Hfail" with "[%] Hreq Hrep").
iDestruct "Hrep" as (??) "(Hrep & Hrep_sl & HΦ)".
iApply ("HΦ" with "Hreq Hrep Hrep_sl").
Global Instance is_urpc_handler_pred_pers f Spec : Persistent (is_urpc_handler_pred f Spec).
Global Typeclasses Opaque is_urpc_handler_pred.
Global Typeclasses Opaque is_urpc_spec_pred.
Section urpc_global_defs.
Context `{HPRE: !gooseGlobalGS Σ}.
Implicit Type (l:list (u64 * savedSpecO Σ (list u8) (list u8))).
Fixpoint is_urpc_spec_pred_list γ host l :=
match l with
| [] => True%I
| x :: l =>
(is_urpc_spec_pred γ host x.1 x.2 ∗ is_urpc_spec_pred_list γ host l)%I
end.
Fixpoint dom_spec_list l : gset u64 :=
match l with
| [] => ∅
| x :: l => {[ x.1 ]} ∪ dom_spec_list l
end.
Fixpoint spec_list_wf l : Prop :=
match l with
| [] => True
| x :: l =>
(x.1 ∉ dom_spec_list l) ∧ spec_list_wf l
end.
Lemma alloc_is_urpc_list_pred (host : chan) specs (Hwf: spec_list_wf specs) :
host c↦ ∅ ={⊤}=∗ ∃ γ,
is_urpc_dom γ (dom_spec_list specs) ∗
is_urpc_spec_pred_list γ host specs.
iMod (map_init (∅ : gmap u64 gname)) as (γmap) "Hmap_ctx".
iMod (own_alloc (to_agree (dom_spec_list specs : gsetO u64))) as (γdom) "#Hdom".
set (Γsrv := {| scmap_name := γmap; scset_name := γdom |}).
iMod (inv_alloc urpc_serverN _ ((server_chan_inner host Γsrv)) with "[Hchan]") as "#Hinv".
rewrite big_sepS_empty //.
iAssert (∀ specs', ⌜ spec_list_wf specs' ⌝ ∗ ⌜ dom_spec_list specs' ⊆ dom_spec_list specs ⌝ →
|==> ∃ gnames : gmap u64 gname, ⌜ dom gnames = dom_spec_list specs' ⌝ ∗
map_ctx (scmap_name Γsrv) 1 gnames ∗
is_urpc_spec_pred_list Γsrv host specs')%I with "[Hmap_ctx]" as "H"; last first.
iMod ("H" with "[]") as (?) "(_&_&$)"; eauto.
iInduction specs' as [| hd spec] "IH".
iMod ("IH" with "[$] []") as (gnames Hdom) "(Hmap_ctx&Hmap)".
destruct Hwf' as (_&?); eauto.
etransitivity; last eassumption.
iMod (saved_spec_alloc hd.2) as (γsave) "#Hsaved".
iMod (map_alloc_ro (hd.1) γsave
with "Hmap_ctx") as "(Hmap_ctx&#Hsaved_name)"; auto.
destruct (Hwf') as (?&?).
rewrite ?dom_insert_L Hdom.