Skip to content

Commit

Permalink
finish locksvc
Browse files Browse the repository at this point in the history
  • Loading branch information
@fhackett
fhackett committed Nov 15, 2024
1 parent 7065304 commit 18034be
Show file tree
Hide file tree
Showing 7 changed files with 425 additions and 46 deletions.
6 changes: 5 additions & 1 deletion .gitignore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -395,4 +395,8 @@ test/files/**/*.txt
*.old

.metals/
.scala-build/
.scala-build/

/.tools/
_apalache-out/
states/
22 changes: 20 additions & 2 deletions systems/locksvc/go.mod
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,13 +4,31 @@ go 1.18

replace github.com/UBC-NSS/pgo/distsys => ../../distsys

require github.com/UBC-NSS/pgo/distsys v0.0.0-20230205084253-49d68d375870
require github.com/UBC-NSS/pgo/distsys v0.0.0-20241028153046-7065304c9763

require (
github.com/benbjohnson/immutable v0.4.3 // indirect
github.com/cespare/xxhash v1.1.0 // indirect
github.com/cespare/xxhash/v2 v2.2.0 // indirect
github.com/dgraph-io/badger/v3 v3.2103.5 // indirect
github.com/dgraph-io/ristretto v0.1.1 // indirect
github.com/dustin/go-humanize v1.0.1 // indirect
github.com/gogo/protobuf v1.3.2 // indirect
github.com/golang/glog v1.0.0 // indirect
github.com/golang/groupcache v0.0.0-20210331224755-41bb18bfe9da // indirect
github.com/golang/protobuf v1.5.2 // indirect
github.com/golang/snappy v0.0.4 // indirect
github.com/google/flatbuffers v23.1.21+incompatible // indirect
github.com/klauspost/compress v1.15.15 // indirect
github.com/pkg/errors v0.9.1 // indirect
github.com/segmentio/fasthash v1.0.3 // indirect
github.com/stretchr/testify v1.8.0 // indirect
github.com/stretchr/testify v1.8.1 // indirect
go.opencensus.io v0.24.0 // indirect
go.uber.org/atomic v1.10.0 // indirect
go.uber.org/multierr v1.9.0 // indirect
golang.org/x/exp v0.0.0-20230213192124-5e25df0256eb // indirect
golang.org/x/net v0.7.0 // indirect
golang.org/x/sync v0.1.0 // indirect
golang.org/x/sys v0.5.0 // indirect
google.golang.org/protobuf v1.28.1 // indirect
)
186 changes: 186 additions & 0 deletions systems/locksvc/go.sum
View file

Large diffs are not rendered by default.

7 changes: 2 additions & 5 deletions systems/locksvc/locksvc.cfg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,13 +4,10 @@ CONSTANT defaultInitValue = defaultInitValue
CONSTANT NumClients = 5

\* SPECIFICATION definition
SPECIFICATION Spec
SPECIFICATION SpecNoDeadlock

\* INVARIANT definition
INVARIANT Safety

\* PROPERTY definition
PROPERTY Liveness

\* CHECK_DEADLOCK setting
CHECK_DEADLOCK FALSE
PROPERTY Liveness
23 changes: 14 additions & 9 deletions systems/locksvc/locksvc.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -199,7 +199,10 @@ var jumpTable = distsys.MakeMPCalJumpTable(
if err != nil {
return err
}
hasLock := iface.RequireArchetypeResource("AClient.hasLock")
hasLock, err := iface.RequireArchetypeResourceRef("AClient.hasLock")
if err != nil {
return err
}
var respRead tla.Value
respRead, err = iface.Read(network3, []tla.Value{iface.Self()})
if err != nil {
Expand All @@ -211,7 +214,7 @@ var jumpTable = distsys.MakeMPCalJumpTable(
return fmt.Errorf("%w: (resp) = (GrantMsg)", distsys.ErrAssertionFailed)
}
// no statements
err = iface.Write(hasLock, nil, tla.ModuleTRUE)
err = iface.Write(hasLock, []tla.Value{iface.Self()}, tla.ModuleTRUE)
if err != nil {
return err
}
Expand All @@ -223,22 +226,25 @@ var jumpTable = distsys.MakeMPCalJumpTable(
Body: func(iface distsys.ArchetypeInterface) error {
var err error
_ = err
hasLock0, err := iface.RequireArchetypeResourceRef("AClient.hasLock")
if err != nil {
return err
}
network4, err := iface.RequireArchetypeResourceRef("AClient.network")
if err != nil {
return err
}
hasLock0 := iface.RequireArchetypeResource("AClient.hasLock")
err = iface.Write(hasLock0, []tla.Value{iface.Self()}, tla.ModuleFALSE)
if err != nil {
return err
}
err = iface.Write(network4, []tla.Value{ServerID(iface)}, tla.MakeRecord([]tla.RecordField{
{tla.MakeString("from"), iface.Self()},
{tla.MakeString("type"), UnlockMsg(iface)},
}))
if err != nil {
return err
}
err = iface.Write(hasLock0, nil, tla.ModuleFALSE)
if err != nil {
return err
}
return iface.Goto("AClient.Done")
},
},
Expand Down Expand Up @@ -266,11 +272,10 @@ var AServer = distsys.MPCalArchetype{
var AClient = distsys.MPCalArchetype{
Name: "AClient",
Label: "AClient.acquireLock",
RequiredRefParams: []string{"AClient.network"},
RequiredRefParams: []string{"AClient.network", "AClient.hasLock"},
RequiredValParams: []string{},
JumpTable: jumpTable,
ProcTable: procTable,
PreAmble: func(iface distsys.ArchetypeInterface) {
iface.EnsureArchetypeResourceLocal("AClient.hasLock", tla.ModuleFALSE)
},
}
65 changes: 36 additions & 29 deletions systems/locksvc/locksvc.tla
View file
Original file line number Diff line number Diff line change
Expand Up @@ -57,35 +57,32 @@ CONSTANT NumClients
};
}
archetype AClient(ref network[_])
variable hasLock = FALSE;
archetype AClient(ref network[_], ref hasLock[_])
{
acquireLock:
network[ServerID] := [from |-> self, type |-> LockMsg];
criticalSection:
with (resp = network[self]) {
assert resp = GrantMsg;
};
hasLock := TRUE;
\* print <<"in critical section: ", self>>;
hasLock[self] := TRUE;
unlock:
hasLock[self] := FALSE;
network[ServerID] := [from |-> self, type |-> UnlockMsg];
hasLock := FALSE;
}
variables network = [id \in NodeSet |-> <<>>];
variables network = [id \in NodeSet |-> <<>>], hasLock = [id \in NodeSet |-> FALSE];
fair process (Server \in ServerSet) == instance AServer(ref network[_])
mapping network[_] via ReliableFIFOLink;
fair process (client \in ClientSet) == instance AClient(ref network[_])
fair process (client \in ClientSet) == instance AClient(ref network[_], ref hasLock[_])
mapping network[_] via ReliableFIFOLink;
}
\* BEGIN PLUSCAL TRANSLATION
--algorithm locksvc {
variables network = [id \in NodeSet |-> <<>>];
variables network = [id \in NodeSet |-> <<>>]; hasLock = [id \in NodeSet |-> FALSE];
define{
ServerID == 0
ServerSet == {ServerID}
Expand Down Expand Up @@ -144,7 +141,6 @@ CONSTANT NumClients
}

fair process (client \in ClientSet)
variables hasLock = FALSE;
{
acquireLock:
with (value10 = [from |-> self, type |-> LockMsg]) {
Expand All @@ -160,14 +156,14 @@ CONSTANT NumClients
resp1 = yielded_network00
) {
assert (resp1) = (GrantMsg);
hasLock := TRUE;
hasLock := [hasLock EXCEPT ![self] = TRUE];
goto unlock;
};
};
unlock:
hasLock := [hasLock EXCEPT ![self] = FALSE];
with (value20 = [from |-> self, type |-> UnlockMsg]) {
network := [network EXCEPT ![ServerID] = Append((network)[ServerID], value20)];
hasLock := FALSE;
goto Done;
};
}
Expand All @@ -176,9 +172,9 @@ CONSTANT NumClients
\* END PLUSCAL TRANSLATION
********************)
\* BEGIN TRANSLATION (chksum(pcal) = "48ee4eec" /\ chksum(tla) = "98748790")
\* BEGIN TRANSLATION (chksum(pcal) = "c964cf97" /\ chksum(tla) = "70ef86db")
CONSTANT defaultInitValue
VARIABLES network, pc
VARIABLES pc, network, hasLock

(* define statement *)
ServerID == 0
Expand All @@ -189,27 +185,26 @@ LockMsg == 1
UnlockMsg == 2
GrantMsg == 3

VARIABLES msg, q, hasLock
VARIABLES msg, q

vars == << network, pc, msg, q, hasLock >>
vars == << pc, network, hasLock, msg, q >>

ProcSet == (ServerSet) \cup (ClientSet)

Init == (* Global variables *)
/\ network = [id \in NodeSet |-> <<>>]
/\ hasLock = [id \in NodeSet |-> FALSE]
(* Process Server *)
/\ msg = [self \in ServerSet |-> defaultInitValue]
/\ q = [self \in ServerSet |-> <<>>]
(* Process client *)
/\ hasLock = [self \in ClientSet |-> FALSE]
/\ pc = [self \in ProcSet |-> CASE self \in ServerSet -> "serverLoop"
[] self \in ClientSet -> "acquireLock"]

serverLoop(self) == /\ pc[self] = "serverLoop"
/\ IF TRUE
THEN /\ pc' = [pc EXCEPT ![self] = "serverReceive"]
ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
/\ UNCHANGED << network, msg, q, hasLock >>
/\ UNCHANGED << network, hasLock, msg, q >>

serverReceive(self) == /\ pc[self] = "serverReceive"
/\ (Len((network)[self])) > (0)
Expand All @@ -218,7 +213,7 @@ serverReceive(self) == /\ pc[self] = "serverReceive"
/\ LET yielded_network1 == readMsg00 IN
/\ msg' = [msg EXCEPT ![self] = yielded_network1]
/\ pc' = [pc EXCEPT ![self] = "serverRespond"]
/\ UNCHANGED << q, hasLock >>
/\ UNCHANGED << hasLock, q >>

serverRespond(self) == /\ pc[self] = "serverRespond"
/\ IF ((msg[self]).type) = (LockMsg)
Expand All @@ -240,7 +235,7 @@ serverRespond(self) == /\ pc[self] = "serverRespond"
/\ UNCHANGED network
ELSE /\ pc' = [pc EXCEPT ![self] = "serverLoop"]
/\ UNCHANGED << network, q >>
/\ UNCHANGED << msg, hasLock >>
/\ UNCHANGED << hasLock, msg >>

Server(self) == serverLoop(self) \/ serverReceive(self)
\/ serverRespond(self)
Expand All @@ -249,7 +244,7 @@ acquireLock(self) == /\ pc[self] = "acquireLock"
/\ LET value10 == [from |-> self, type |-> LockMsg] IN
/\ network' = [network EXCEPT ![ServerID] = Append((network)[ServerID], value10)]
/\ pc' = [pc EXCEPT ![self] = "criticalSection"]
/\ UNCHANGED << msg, q, hasLock >>
/\ UNCHANGED << hasLock, msg, q >>

criticalSection(self) == /\ pc[self] = "criticalSection"
/\ (Len((network)[self])) > (0)
Expand All @@ -258,15 +253,15 @@ criticalSection(self) == /\ pc[self] = "criticalSection"
/\ LET yielded_network00 == readMsg10 IN
LET resp1 == yielded_network00 IN
/\ Assert((resp1) = (GrantMsg),
"Failure of assertion at line 162, column 11.")
"Failure of assertion at line 158, column 11.")
/\ hasLock' = [hasLock EXCEPT ![self] = TRUE]
/\ pc' = [pc EXCEPT ![self] = "unlock"]
/\ UNCHANGED << msg, q >>

unlock(self) == /\ pc[self] = "unlock"
/\ hasLock' = [hasLock EXCEPT ![self] = FALSE]
/\ LET value20 == [from |-> self, type |-> UnlockMsg] IN
/\ network' = [network EXCEPT ![ServerID] = Append((network)[ServerID], value20)]
/\ hasLock' = [hasLock EXCEPT ![self] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "Done"]
/\ UNCHANGED << msg, q >>

Expand All @@ -288,16 +283,28 @@ Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION

ServerIsIdle ==
\E self \in ServerSet :
/\ pc[self] = "serverReceive"
/\ UNCHANGED vars

SpecNoDeadlock ==
/\ Init
/\ [][Next \/ ServerIsIdle]_vars
/\ \A self \in ServerSet : WF_vars(Server(self))
/\ \A self \in ClientSet : WF_vars(client(self))

\* Invariants

Safety == \lnot (\A i, j \in ClientSet:
/\ i /= j
/\ hasLock[i]
/\ hasLock[j])
Safety ==
\A i, j \in ClientSet:
(/\ i # j
/\ hasLock[i])
=> ~ hasLock[j]

\* Properties

ProgressOK(i) == pc[i] = "acquireLock" ~> pc[i] = "criticalSection"
ProgressOK(i) == pc[i] = "acquireLock" ~> (pc[i] = "criticalSection" ~> pc[i] = "unlock")
Liveness == \A i \in NodeSet: ProgressOK(i)

=============================================================================
Loading

0 comments on commit 18034be

Please sign in to comment.