---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/AllocatorImplementation.tla
---
------------------------ MODULE AllocatorImplementation ------------------------
(***********************************************************************)
(* Specification of an allocator managing a set of resources: *)
(* - Clients can request sets of resources whenever all their previous *)
(* requests have been satisfied. *)
(* - Requests can be partly fulfilled, and resources can be returned *)
(* even before the full request has been satisfied. However, clients *)
(* only have an obligation to return resources after they have *)
(* obtained all resources they requested. *)
(* This allocator operates by repeatedly choosing a schedule according *)
(* to which requests are satisfied. Resources can be allocated out of *)
(* order as long as no client earlier in the schedule asks for them. *)
(* This module adds communication between the allocator and the client *)
(* processes, which now hold some local state. *)
(***********************************************************************)
EXTENDS FiniteSets, Sequences, Naturals
CONSTANTS
Clients, \* set of all clients
Resources \* set of all resources
ASSUME
IsFiniteSet(Resources)
VARIABLES
(** variables held by the allocator **)
unsat, \* set of all outstanding requests per process
alloc, \* set of resources allocated to given process
sched, \* schedule represented as a sequence of clients
(** variables of the clients **)
requests, \* pending requests per client
holding, \* resources currently held by the client
(** communication network between clients and allocator **)
network \* set of messages in transit
Sched == INSTANCE SchedulingAllocator
--------------------------------------------------------------------------------
Messages ==
[type: {"request", "allocate", "return"},
clt: Clients,
rsrc: SUBSET Resources]
TypeInvariant ==
/\ Sched!TypeInvariant
/\ requests \in [Clients -> SUBSET Resources]
/\ holding \in [Clients -> SUBSET Resources]
/\ network \in SUBSET Messages
--------------------------------------------------------------------------------
(* Initially, no resources have been requested or allocated. *)
Init ==
/\ Sched!Init
/\ requests = [c \in Clients |-> {}]
/\ holding = [c \in Clients |-> {}]
/\ network = {}
(* A client c may request a set of resources provided that it has *)
(* neither pending requests nor holds any resources. The request is *)
(* put into the network for delivery to the allocator. *)
Request(c, S) ==
/\ requests[c] = {} /\ holding[c] = {}
/\ S /= {} /\ requests' = [requests EXCEPT ![c] = S]
/\ network' = network \union {[type |-> "request", clt |-> c, rsrc |-> S]}
/\ UNCHANGED << unsat, alloc, sched, holding >>
(* Reception of a request message from a client by the allocator. *)
(* The allocator updates its data structures and inserts the client *)
(* into the pool of clients with pending requests. *)
RReq(m) ==
/\ m \in network /\ m.type = "request"
/\ alloc[m.clt] = {} \** don't handle request messages prematurely(!)
/\ unsat' = [unsat EXCEPT ![m.clt] = m.rsrc]
/\ network' = network \ {m}
/\ UNCHANGED << alloc, sched, requests, holding >>
(* Allocation of a set of available resources to a client that has *)
(* requested them (the entire request does not have to be filled). *)
(* The process must appear in the schedule, and no process earlier in *)
(* the schedule may have requested one of the resources. *)
Allocate(c, S) ==
/\ Sched!Allocate(c,S)
/\ network' = network \union {[type |-> "allocate", clt |-> c, rsrc |-> S]}
/\ UNCHANGED << requests, holding >>
(* Reception of an allocation message by a client. *)
RAlloc(m) ==
/\ m \in network /\ m.type = "allocate"
/\ holding' = [holding EXCEPT ![m.clt] = @ \union m.rsrc]
/\ requests' = [requests EXCEPT ![m.clt] = @ \ m.rsrc]
/\ network' = network \ {m}
/\ UNCHANGED << unsat, alloc, sched >>
(* Client c returns a set of resources that it holds. It may do so *)
(* even before its full request has been honored. *)
Return(c, S) ==
/\ S /= {} /\ S \subseteq holding[c]
/\ holding' = [holding EXCEPT ![c] = @ \ S]
/\ network' = network \union {[type |-> "return", clt |-> c, rsrc |-> S]}
/\ UNCHANGED << unsat, alloc, sched, requests >>
(* Reception of a return message by the allocator. *)
RRet(m) ==
/\ m \in network /\ m.type = "return"
/\ alloc' = [alloc EXCEPT ![m.clt] = @ \ m.rsrc]
/\ network' = network \ {m}
/\ UNCHANGED << unsat, sched, requests, holding >>
(* The allocator extends its schedule by adding the processes from *)
(* the pool (that have outstanding requests but that have not yet been *)
(* scheduled, in some unspecified order. *)
Schedule ==
/\ Sched!Schedule
/\ UNCHANGED << requests, holding, network >>
(* The next-state relation per client and set of resources. *)
Next ==
\/ \E c \in Clients, S \in SUBSET Resources:
Request(c, S) \/ Allocate(c, S) \/ Return(c, S)
\/ \E m \in network:
RReq(m) \/ RAlloc(m) \/ RRet(m)
\/ Schedule
vars == << unsat, alloc, sched, requests, holding, network >>
--------------------------------------------------------------------------------
(***********************************************************************)
(* Liveness assumptions: *)
(* - Clients must return resources if their request has been satisfied.*)
(* - The allocator must eventually allocate resources when possible. *)
(* - The allocator must schedule the processes in the pool. *)
(* - Messages must eventually be received. *)
(***********************************************************************)
Liveness ==
/\ \A c \in Clients: WF_vars(requests[c] = {} /\ Return(c, holding[c]))
/\ \A c \in Clients: WF_vars(\E S \in SUBSET Resources: Allocate(c, S))
/\ WF_vars(Schedule)
/\ \A m \in Messages:
/\ WF_vars(RReq(m))
/\ WF_vars(RAlloc(m))
/\ WF_vars(RRet(m))
(* The specification of the entire system *)
Specification == Init /\ [][Next]_vars /\ Liveness
--------------------------------------------------------------------------------
RequestsInTransit(c) == \** requests sent by c but not yet received
{msg.rsrc: msg \in {m \in network: m.type = "request" /\ m.clt = c}}
AllocsInTransit(c) == \** allocations sent to c but not yet received
{msg.rsrc: msg \in {m \in network: m.type = "allocate" /\ m.clt = c}}
ReturnsInTransit(c) == \** return messages sent by c but not yet received
{msg.rsrc: msg \in {m \in network: m.type = "return" /\ m.clt = c}}
Invariant == \** a lower-level invariant
(** invariants for the allocator's data structures as before **)
/\ Sched!AllocatorInvariant
(** interplay between allocator and client variables **)
/\ \A c \in Clients:
/\ Cardinality(RequestsInTransit(c)) <= 1
/\ requests[c] = unsat[c]
\union UNION RequestsInTransit(c)
\union UNION AllocsInTransit(c)
/\ alloc[c] = holding[c]
\union UNION AllocsInTransit(c)
\union UNION ReturnsInTransit(c)
(* correctness properties in terms of clients' variables *)
ResourceMutex ==
\A c1, c2 \in Clients: holding[c1] \intersect holding[c2] /= {} => c1 = c2
ClientsWillReturn ==
\A c \in Clients: (requests[c] = {} ~> holding[c] = {})
ClientsWillObtain ==
\A c \in Clients, r \in Resources: r \in requests[c] ~> r \in holding[c]
InfOftenSatisfied ==
\A c \in Clients: []<>(requests[c] = {})
--------------------------------------------------------------------------------
THEOREM Specification => []TypeInvariant
THEOREM Specification => []ResourceMutex
THEOREM Specification => []Invariant
THEOREM Specification => ClientsWillReturn
THEOREM Specification => ClientsWillObtain
THEOREM Specification => InfOftenSatisfied
--------------------------------------------------------------------------------
(* This implementation is a refinement of the scheduling allocator. *)
SchedAllocator == Sched!Allocator
THEOREM Specification => SchedAllocator
================================================================================