STaVe: the SyncTask Verifier
STaVe is a tool that verifies the correct usage of condition variables (CVs). In the Java world, CVs are either monitors, i.e., synchronization objects with wait / notify / notifyAll capability, or Condition objects (from java.util.concurrency). By correctness, we mean the (here stated informally) property that All threads synchronizing under the same set of condition variables will eventually exit its synchronization block. I.e., no waiting thread will starve indefinitely because it will not be notified.
STaVe provides an annotation language on top of Java source programs to define the expected thread synchronization using condition variables. It takes as input the annotated code, and extracts the expected synchronization scheme as a SyncTask program. SyncTask is a non-procedural Java-like imperative language to define synchronization schemes using condition. The language captures only the relevant aspects of synchronization, namely the synchronization mechanisms (locks and CVs), and the control-flow structure and variables. One can see SyncTask as an abstraction from the original program synchronization. E.g., if the predicate that determines if a thread will notify or will wait is "buffer is full" or "buffer is empty", in SyncTask the list content is ignored, and the only information preserved is the list size. Then, the tool translates SyncTask programs into a Coloured Petri Nets (CPN), that is input it to CPN Tools, which verifies the CPN and prove/disprove the correct usage of CVs.
STaVe is written in Java. It depends on Java Parser for AST generation, and on OpenJDK Javac for type-checking. The library javaparser2jctree converts a Java Parser AST into a Javac AST, and is a spin-off from STaVe. Another spin-off is the libcpntools library, which generates coloured Petri net files in CPN Tool's ".cpn" format.
As future work, we plan to extend the annotation language and SyncTask extraction to C and C++ programs synchronizing via POSIX condition variables. Moreover, we would like to support other CPN analysis tools, such as PIPE. It is also in our plans the output for model checkers, such as Spin (Promela) or NuSMV.
Last Modified: April 30 2017.