Commit 621a41d6 authored by Jonas Kastberg's avatar Jonas Kastberg

More nits and consistency of CoqDoc

parent 34d30758
......@@ -9,14 +9,14 @@ The main difference is that the protocols are defined over predicates,
in place of types.
Dependent Separation Protocols are modelled as the following type:
- [proto] := 1 + ([action] * (V → (▶ [proto] → PROP) → PROP))
- [proto := 1 + (action * (V → (▶ proto → PROP) → PROP))]
Here the left-hand side of the sum is used for the terminated process,
while the right-hand side is used for the communication constructors.
[action] is an inductively defined datatype with two constructors,
that is used to differentiate between sending and received, rather than
having two distinct sums in [proto].
- [action] := [Send] | [Receive]
- [action := Send | Receive]
The remainder (V → (▶ [proto] → PROP) → PROP)) is a continuation that
depends on the communicated value V and the dependent tail (▶ proto → PROP)
......
(** This file provides utility for defining and using
the commonly used ghost functor over authoritative exclusive ownership. *)
a commonly used ghost functor over authoritative exclusive ownership.
[AuthExcl A := Auth (Option (Excl A))]
This is isomorphic to a half-ownership, with an intuitive
use-case, being putting the authoritative part in an
invariant, while giving the other fragment to the client
with write permissions. *)
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl auth.
From iris.base_logic.lib Require Import own.
......
(** This file defines a ghost functor for tracking
"contributions" made to a shared concurrent effort.
It is ultimately defined as:
contribution := Auth (Option ((Pos * A) + Excl 1))
Intuitively it allows one to allocate a [server] and
a number of [client] fragments. The server keeps track
of the number of active clients, and what resources they
are currently holding.
To deallocate a client it must hold no resources.
To deallocate a server there must be no remaining clients.
[contribution := Auth (Option ((Pos * A) + Excl 1))]
Intuitively it allows one to allocate a [server] and a
number of [client] fragments, where the server keeps
track of the number of active clients, and what resources
they are currently holding.
*)
From iris.base_logic Require Export base_logic lib.iprop lib.own.
From iris.proofmode Require Export tactics.
......
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