[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Launching two sets of processes from the same base set in PlusCal



Consider a protocol similar to Paxos, where each node in the cluster runs multiple processes concurrently - Proposer and Acceptor. The two processes access shared memory, maybe a local database. We might write this as follows:

----------------------------- MODULE Example -----------------------------

CONSTANTS Node, Value

NoValue == CHOOSE v : v \notin Value

(*--algorithm Example

variables
    sharedMemory = [n \in Node |-> NoValue]

process Acceptor \in Node
begin
    RunAcceptor:
        \* Do something with sharedMemory[self] here
        skip;
end process;

process Proposer \in Node
begin
    RunProposer:
        \* Do something with sharedMemory[self] here
        skip;
end process;

end algorithm;*)

=============================================================================

PlusCal doesn't allow this, because its PC function maps elements of Node to only one value so the two processes cannot run concurrently. What is the best way to accomplish what I'm trying to do?

Andrew

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/efdac118-b42a-4da7-8fc2-2872f4d73369%40googlegroups.com.