Synchronisers: CountDownLatch

Verifying a Java implementation of a countdown latch. The verification uses witness encoding and handles atomic operations (CAS, axiomatised).

General information

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

Statistical information

Lines of code101 lines (comments not included)
Lines of specification60 lines (59.41% of the total)
Computation time19712 milliseconds

Example code

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