Synchronisers: ReentrantLock

In this example case a re-entrant lock, implemented in Java, is verified. An atomic integer is used as the synchroniser.

General information

ID149
Articlenone
Back-endChalice
LanguageJava
FeaturesAtomics, Locking, Loop invariants, Witnesses
Sources
Path to example filesynchronizers/ReentrantLock.java
Date2017-06-21

Statistical information

Lines of code140 lines (comments not included)
Lines of specification81 lines (57.86% of the total)
Computation time20853 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.