School of
Computer Science
and Communication
About
Team
Download
Examples
Documentation
KTH
/
CSC
/
TCS
/
People
/
Pedro
/ STaVe
STaVe: the SyncTask Verifier
Example
Description
Annotated Java
SynckTask
Coloured Petri Net
Graphic
Barrier
Implementation of barrier for 10 threads
N/A
Barrier.syn
Barrier.cpn
N/A
Buffer sharing
Producer and Consumer threads compete for adding / removing elements in a bounded buffer
ProdCons.java
ProdCons.syn
ProdCons.cpn
(hierarchical)
FlattenedProdCons.cpn
(non-hierarchical)
FlattenedProdCons.pdf
Lock-Based FIFO Queue
Producer / Consumer threads compete for adding / removing elements in a bounded FIFO. Sync uses 1 lock with 2 condvars
LockBasedFifo.java
LockBasedFifo.syn
LockBasedFifo.cpn
(hierarchical)
N/A
Loop
Threads loop forever waiting/notifying each other
N/A
Loop.syn
Loop.cpn
N/A
Nested
Synchronization using nested synchronized blocks
N/A
Nested.syn
Nested.cpn
N/A
Last Modified: May 13 2016.
