Skip to content
Snippets Groups Projects

Added close definition and spec

Open Jonas Kastberg requested to merge close_spec into master
All threads resolved!

Added a definition and specification for "closing" channels. The idea is that a channel endpoint, once it reaches END can guarantee that its inbound buffer (i.e. vsr for Left, and vsl for Right) is empty, and is no longer used by either party. As such, it can Free the buffer (using the primitive Free instruction) to deallocate the memory. In doing so, it gives up its endpoint ownership c >-> END.

This is achieved by changing the channel invariant to either hold the buffers, or the terminated channel endpoint:

Definition iProto_mapsto_def `{!heapGS Σ, !chanG Σ}
    (c : val) (p : iProto Σ) : iProp Σ :=
  ∃ γ s (l r : loc) (lk : val),
    ⌜ c = ((#(side_elim s l r), #(side_elim s r l)), lk)%V ⌝ ∗
    is_lock (chan_lock_name γ) lk (∃ vsl vsr,
      (llist internal_eq l vsl ∨ iProto_own (chan_proto_name γ) Right END%proto) ∗
      (llist internal_eq r vsr ∨ iProto_own (chan_proto_name γ) Left END%proto) ∗
      steps_lb (length vsl) ∗ steps_lb (length vsr) ∗
      iProto_ctx (chan_proto_name γ) vsl vsr) ∗
    iProto_own (chan_proto_name γ) s p.

The proof relies on three observations:

  • We can always receive (e.g. on vsr for Left), as we can derive a contradiction between our local endpoint ownership, and the one in the invariant. (new lemma iProto_own_exclusive)
  • We can always send (e.g. on vsl for Left), as we can derive that whenever one protocol is sending (i.e. (<! xs> MSG v {{ P }} ; p), then the other protocol has not terminated (i.e. it is not END), and so it cannot be in the invariant. (new lemmas iProto_interp_send_end_inv_{l,r})
  • When our endpoint is END, the inbound buffer is always empty, and so we can close it without worrying about leftover resources (new lemmas iProto_interp_end_inv_{l,r}).

EDIT: Closed the outstanding lemmas

Edited by Jonas Kastberg

Merge request reports

Ready to merge by members who can write to the target branch.
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Robbert Krebbers
  • Jonas Kastberg added 2 commits

    added 2 commits

    • bdb8f212 - Closed proof of exclusivity of iProto_own
    • 1dd20dfc - Fixed wrong argument scope and clean up

    Compare with previous version

  • Jonas Kastberg resolved all threads

    resolved all threads

  • Jonas Kastberg changed title from WIP: Added close spec with outstanding admitted lemmas to Added close definition and spec

    changed title from WIP: Added close spec with outstanding admitted lemmas to Added close definition and spec

  • Jonas Kastberg changed the description

    changed the description

  • Please register or sign in to reply
    Loading