-
Notifications
You must be signed in to change notification settings - Fork 26
Atomics and Locks
VerCors supports three forms of synchronization primitives. Two can only be used in PVL, one can only be used in Java. Each form will be discussed individually.
Intrinsic locking in PVL consists of three parts:
- Lock invariants
- The
lock
statement - The
unlock
statement
A lock invariant can be defined within a class with the following syntax:
class C {
...
resource lock_invariant() = /* resource expression involving permissions and boolean assertions */ ;
...
}
This syntax is very similar to the syntax used for defining predicates. You can find more info about predicates here. However, knowledge of predicates is not needed to understand and use locks in VerCors.
Because a lock invariant is defined in a class, it is always related to a specific class instance. Therefore, it is possible to make assertions about instance fields in the lock invariant. For example, a lock invariant could be specified that contains the permissions for a field, and also the fact that that field must have a value greater than 10, using the following syntax:
class C {
int f;
resource lock_invariant() = Perm(f, write) ** f > 10;
}
A lock
Tutorial
- Introduction
- Installing and Running VerCors
- Prototypical Verification Language
- Specification Syntax
- Permissions
- GPGPU Verification
- Axiomatic Data Types
- Arrays and Pointers
- Parallel Blocks
- Atomics and Locks
- Process Algebra Models
- Predicates
- Inheritance
- Exceptions & Goto
- VerCors by Error
- VeyMont
- Advanced Concepts
- Annex
- Case Studies
Developing for VerCors