Try our resource analyzer from the following form.
P ::= O (inaction. the 15th letter of the English alphabet, not 0)
| x!(v1,v2,...,vn).P (output)
| x?(x1,x2,...,xn).P (input)
| P1 | P2 (parallel composition)
| new x in P (channel creation)
| newR specification, x in P (resource creation)
| acc(v, <access label>).P (resource access)
| if v then P1 else P2 (conditional)
| *P (replication)
| (P) (the same as P)
v ::= () (unit)
| true (boolean values)
| false
| x (variables)
| (v) (the same as v)
specification ::= { regexp } (specification in a regular expression)
| <integer> (pre-defined specification)
regexp ::= <access label> (single access)
| regexp ... regexp (sequence)
| regexp * (repetition)
| regexp | regexp (choice)
| (regexp) (the same as regexp)
<access label> is a string of lowercase letters. Specification in the resource creation syntax is either a regular expression over access labels or an integer (1 or 2). Each integer is interpreted as follows:
Trailing "O" may be omitted, so that you can write, for example, x!(true) instead of x!(true).O.
The following process first creates a resource x that should be first initialized, read an arbitrary number of times, and then closed. It then spawns four processes; they synchronize through channels c1 and c2, so that x is accessed in a valid order.
newR 1, x in new c1 in new c2 in acc(x, init).(c1!() | c1!()) | c1?().acc(x, read).c2!() | c1?().acc(x, read).c2!() | c2?().c2?().acc(x, close)
The program above is equivalent to the following program.
newR { init (read|write)* close }, x in
new c1 in
new c2 in
acc(x, init).(c1!() | c1!()) |
c1?().acc(x, read).c2!() |
c1?().acc(x, read).c2!() |
c2?().c2?().acc(x, close)
The following program is prototypical of recursive functions. There is a replicated service which listens on channel repeat_read; it either terminates the recursion by sending a message back on the reply channel r, or it recursively invokes a sub-instance of itself which will reply on a private channel r2. In this example each recursive step does a acc(x, read).
new repeat_read in *(repeat_read?(b, x, r). if b then r!() else (new r2 in (repeat_read!(b, x, r2) | r2?().acc(x, read).r!()))) | (newR 1, y in new rep in (acc(y, init).repeat_read!(b, y, rep) | rep?().acc(y, close)))
The analyzer reports that partial liveness is not verified for the example above. This occurs due to the limitation of TyPiCal, the deadlock-freedom analyzer used in our resource usage analyzer. (TyPiCal cannot verify that r2?() succeeds.)
Partial liveness can be verified for the following two programs, which are similar to the previous program.
new repeat in *(repeat?(b,x,r). if b then r!() else acc(x, read).repeat!(b,x,r)) | newR 1, x in new r in (acc(x, init).repeat!(b,x,r) | r?().acc(x,close))
new repeat in
new repeat_read in
*(repeat_read?(b, x, r).if b then r!() else (acc(x,read).repeat_read!(b,x,r))) |
*(repeat?(b).if b then O else
(repeat!(b) |
(newR 1, y in new c1 in new c2 in
(acc(y,init).(c1!() | c1!()) |
c1?().repeat_read!(b,y,c2) |
c1?().repeat_read!(b,y,c2) |
c2?().c2?().acc(y,close))))) |
repeat!(b)
We can verify safety and partial liveness for the following program. The first process runs a server, which returns a new, initialized resource. The second process runs infinitely many client processes, each of which sends a request for a new resource, and after receiving it, reads and closes it. Note that the following program creates infinitely many resources and has infinitely many states.
new create in
new s in
*(create?(r).newR 1,x in acc(x,init).r!(x))
| *(new r in create!(r)
| r?(y).new c in s!(b,y,c) | s!(b,y,c)
| c?().c?().acc(y,close))
| *(s?(b,x,r).if b then r!()
else acc(x,read).s!(b,x,r))
Our analyzer can verify safety and partial liveness for the following producer/consumer program.
new producer in
new consumer in
*producer?(b,p,c).p?().acc(b, put).(c!() | producer!(b,p,c)) |
*consumer?(b,p,c).c?().acc(b, get).(p!() | consumer!(b,p,c)) |
newR 2, buf in new x in new y in
*(producer!(buf,x,y)) | *(consumer!(buf,x,y)) | x!()