fhackett
commented
6 years ago Here is a more fleshed out example of the transformation.
Before
--algorithm counter {
variables counter = 0;
process (P \in 0..procs-1)
variables i = 0;
{
w: while (i < iters) {
incCounter: counter := counter + 1;
print counter;
nextIter: i := i + 1;
}
}
}After
--algorithm counter {
archetype P(self, counter, iters)
variables i = 0;
{
w: while (i < iters) {
incCounter: counter := counter + 1;
print counter;
nextIter: i := i + 1;
}
}
(** testing **)
variables counter = 0;
process (P \in 0..procs-1) = instance P(self, counter, iters);
}Now, if you wanted to use this algorithm from another PlusCal module:
--algorithm UseCounter {
import counter;
(** counter is not very useful, so we just demonstrate another process reading the variable **)
process (Q \in 0..procs-1) = instance P(self, counter, iters);
process (Observer = -1)
variables i = 0;
{
w: while( i < iters ) {
i := i+1;
print counter;
}
}
}Or if you want to use it from custom Go code (code is approximate, precise model for "global" variables needs work):
import "counter"
var counter int = 0;
func main(){
// you can do anything here (incl. goroutines), but for simplicity we just call P directly
counter.P(counter.MakeContext(/*TBD*/), 1, &counter, 15)
}Here is an approximation of counter.go:
package counter
func P(/*context, TBD */, self int, counter *int, int iters){
// generated code goes here
}
rmascarenhas
This issue documents my proposal to extend the PlusCal language with features that enable composability.
Currently one PlusCal algorithm cannot interact with another in any way. They cannot refer to each other during model checking, and there is no consistent way to link PGo-compiled implementations together via shared variables since the algorithms assume exclusive access and this is liable to break invariants without significant modifications to the generated code.
The minimal set of features required for PlusCal to support modules are:
Example of what a PlusCal developer would do in order to use these things, assuming they are writing a system like RAFT where all the processes have the same code:
Hopefully this give a decent outline of what I'm talking about - let me know if anything is unclear.