Commit 2c2d38c5 authored by Robbert Krebbers's avatar Robbert Krebbers

Tweak comments of `channel/channel.v`.

parent 8afdb110
(** This file contains the definition of the Channel language encoding, (** This file contains the definition of the channels, encoded as a pair of
being a pair of buffers, with the three message-passing primitives lock-protected buffers, on which we define the three message-passing primitives:
[new_chan], [send] and [receive], along with their respective specifications.
The abstract representation of a channel endpoint is two buffer references - [new_chan] creates references to two empty buffers and a lock, and returns a
and a lock. [new_chan] creates references to two empty buffers and a lock, and pair of endpoints, where the order of the two references determines the
returns a pair of such endpoints, where the order of the two references polarity of the endpoints.
determines the polarity of the endpoints. - [send] takes an endpoint and adds an element to the first buffer.
- [recv] performs a busy loop until there is something in the second buffer,
The [send] primitive takes such an endpoint abstraction and adds an element to which it pops and returns, locking during each peek.
the first buffer under the lock. Conversely [recv] loops until there is
something in the second buffer, which it pops and returns, locking during
each peek.
The specifications are defined in terms of the logical connectives [is_chan] The specifications are defined in terms of the logical connectives [is_chan]
and [chan_own], which respectively determines the contents of a channel using and [chan_own]:
a lock over an invariant and the ownership of it using ghost fragments
over buffers. - [is_chan γ v1 v2] is a persistent proposition expressing that [v1] and [v2]
*) are the endpoints of a channel with logical name [γ].
- [chan_own γ s vs] is an exclusive proposition expressing the buffer of side
[s] ([Left] or [Right]) has contents [vs]. *)
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock. From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import excl auth list. From iris.algebra Require Import excl auth list.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment