|
|
Some Examples
Syntax
(programs) P ::= C1 C2 ... Cn main
(classes) C ::= class cname <g1,...,gn>{
F1,...,Fn
M1,...,Mm
}
(types) T ::= C<g1,...,gn>
(fields) F ::= T fname
(methods) M ::= mname(T1 a1,..., Tn an)
p(this), p1(a1),...pn(an) => p'(this), p1'(a1),...pn'(an) {
s
}
(constr.) CTR ::= cname(T1 a1,..., Tn an)
none(this), p1(a1),...pn(an) => p'(this), p1'(a1),...pn'(an) {
s
}
(main) main ::= main<g1,...,gn>{
s
}
(refs) r ::= x | x.a | this | this.a
(RHS) rhs ::= r | null
(stat.) s ::= let T1 x1 ... Tn xn in s end
| r<g> := rhs
| r.m(r1,...,rn)
| r := new c<g1,...gm>(r1,...,rn)
| split<g1,...gm>{ s }
(perm) p ::= unq | shr@g | imm | none
|
| Trace | Store
|
|
|
|
|
Summary
|
|
|
Trace
The trace contains certain constraints that help to understand the behavior of the program:
- calling(X,method_name,Z-Line): The reference "X" calls the method "method_name". The 3rd argument helps to know the line of the source code containing the call.
- running(X,method_name,Z-Line): The body of the method "method_name" invoked by "X" is currently running.
- ended(X,method_name,Z-Line): The body of the method "method_name" invoked by "X" terminated.
- AND[ref(X,O,P,G), ct(O,N)]: Before destroying the variable "X",it was pointing to object O with permission P on group G. ct(O,N) tells that there were N references pointing to O.
- ok(): This constraint is added to the store iff all the statements in the main code were executed.
was destroyed a
calling(PC_662,producerconsumer_producerconsumer,line 70 (Z_PAR_951))
ended(B_763,buffer_buffer,line 69 (Z_PAR_850))
The output also shows when the Linear CCP program ends with suspended processes. The remaining suspended processes are killed by the scheduler and reported in the output as "[Killed] ask constraint then ... "
Store
In this section of the output the final store of the Linear CCP program is output. Here, N#C means that there are "N" copies of the constraint C in the store. inf#C means that C is a replicated constraint.
Summary
The summary section shows the state of the variables created by the
program.
|
| Process Definitions
| Main Process
|
|
|
|
| .SIG
| .MOD
|
|
|
|
Calling the Prover
- Download the prover here
(illf.mod, illf.sig, blists.mod, blists.sig)
- Copy the .sig (resp .mod) output above into the file
ALCOVE.sig (resp. ALCOVE.mod).
- Compile the files:
- tjcc blists && tjlink blists
- tjcc illf && tjlink illf
- tjcc ALCOVE && tjlink ALCOVE
- Startup lprolog: tjsim ALCOVE
- Type a goal. Some examples:
- Termination analysis: pv ok.
- The method m of the class c was executed: pv (sigma X \ sigma Z \ ( running X c_m_p Z )).
|
General Description
ALCOVE (Access Permission Linear COnstraints VErifier)
is a framework for the automatic analysis of Access Permission
based programs. The tool comprises a simulator and a prover:
- ALCOVE LCC Animator generates a specification of the
Access Permission (AP) model as agents in Linear Concurrent
Constraint Programming (lcc) [FRS01]. The lcc model is then
used to compute the flow of permissions and animate the
execution of the program.
- From the lcc model, ALCOVE LL Prover generates the
proof obligations for the Focused Linear Logic [And92] theorem
prover written in Lambda-Prolog to verify relevant properties
of the program such us:
- Deadlocks: the program cannot terminate.
- Concurrent executions: whether two methods can be executed concurrently.
- Method Specifications : whether specifications adhere the intended semantics associated with access permissions or not.
Alcove is based on the LCC model and the results reported in [OPRC12].
Please contact Carlos Olarte if you need the source code or you have any problem using the tool.
Syntax of Programs
Access Permission Programs can be written by following the syntax below:
(programs) P ::= C1 C2 ... Cn main
(classes) C ::= class cname <g1,...,gn>{
F1,...,Fn
M1,...,Mm
}
(types) T ::= C<g1,...,gn>
(fields) F ::= T fname
(methods) M ::= mname(T1 a1,..., Tn an)
p(this), p1(a1),...pn(an) => p'(this), p1'(a1),...pn'(an) {
s
}
(constr.) CTR ::= cname(T1 a1,..., Tn an)
none(this), p1(a1),...pn(an) => p'(this), p1'(a1),...pn'(an) {
s
}
(main) main ::= main<g1,...,gn>{
s
}
(refs) r ::= x | x.a | this | this.a
(RHS) rhs ::= r | null
(stat.) s ::= let T1 x1 ... Tn xn in s end
| r<g> := rhs
| r.m(r1,...,rn)
| r := new c<g1,...gm>(r1,...,rn)
| split<g1,...gm>{ s }
(perm) p ::= unq | shr@g | imm | none
For instance:
// Example of Collections
class stats{
stats() this none->unq { }
}
class collection{
collection() this none->unq { }
sort() this unq->unq { }
print() this imm->imm { }
compStats(stats:s) this imm->imm s unq->unq { }
removeDuplicates() this unq->unq { }
}
main<g> {
let collection:c stats:s in {
c := new collection();
s := new stats();
c.sort();
c.print();
c.compStats(s);
c.removeDuplicates();
}
}
Tools
- The Access Permission program is translated to LCC processes with the help of an ANTLR parser.
- The LCC model is executed on LolliP, a Linear CCP interpreter
- The prover was written in Teyjus, an efficient implementation of the higher-order logic programming language Lambda Prolog.
References
|
[OPRC12]
|
C. Olarte, E. Pimentel, C. Rueda, N. Cataño: A
linear concurrent constraint approach for the automatic verification
of access permissions. PPDP 2012: 207-216
N. Cataño, C. Olarte, E. Pimentel and C. Rueda.
A Linear Concurrent Constraint approach for the automatic verification of access permissions.
ACM PPDP'12, 2012. (PDF)
|
|
[SMA09]
|
S. Stork, P. Marques, and J. Aldrich. Concurrency by default: using per- missions to express dataflow in stateful programs. In Proc. of OOPSLA'09, 2009.
|
|
[FRS01]
|
Francois Fages, Paul Ruet, and Sylvain Soliman. Linear concurrent constraint pro-
gramming: Operational and phase semantics. Information and Computation, 165,
2001.
|
|
[And92]
|
Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297-347, 1992.
|