Commit 023322d5 authored by Jonas Kastberg's avatar Jonas Kastberg

Minor updates to contribution

parent 621a41d6
...@@ -3,11 +3,15 @@ ...@@ -3,11 +3,15 @@
It is ultimately defined as: It is ultimately defined as:
[contribution := Auth (Option ((Pos * A) + Excl 1))] [contribution := Auth (Option ((Pos * A) + Excl 1))]
Intuitively it allows one to allocate a [server] and a Intuitively it allows one to allocate a [server γ n v] and a
number of [client] fragments, where the server keeps number of [client γ v] fragments that can each hold resources.
track of the number of active clients, and what resources The intended use is to allocate a client for each thread that
they are currently holding. contributes to a channel endpoint, where the resources [v] are
*) things that are currently owned by the thread, that is later
used in the protocol.
The server keeps track of the number of active clients [n],
and what resources they are currently holding [v].*)
From iris.base_logic Require Export base_logic lib.iprop lib.own. From iris.base_logic Require Export base_logic lib.iprop lib.own.
From iris.proofmode Require Export tactics. From iris.proofmode Require Export tactics.
From iris.algebra Require Import excl auth csum gmultiset frac_auth. From iris.algebra Require Import excl auth csum gmultiset frac_auth.
......
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