Examples
Here you can download some examples running on LEAP. The examples include concurrent and sequential programs.
Safety Verification for Concurrent Programs
The concurrent examples for safety verification include:
- An implementation of a concurrent lock-coupling single-linked lists. More information regarding this example can be found on this paper.
- An implementation of a coarse-grained unbounded concurrent queue
- A lock-free stack implementation
- An implementation of a lock-free non-blocking queue
- A simple mutual exclusion algorithm based on tickets implemented with integers.
- A simple mutual exclusion algorithm based on tickets implemented with sets of integers.
| title | description |
|---|---|
| list | Concurrent lock-coupling single-linked lists |
| unbounded-queue | Concurrent coarse-grained lock-based unbounded queues |
| lock-free stack | Concurrent lock-free stacks |
| lock-free queue | Concurrent lock-free non-blocking queues |
| ticketint | Mutual exclusion algorithm based on tickets using integers |
| ticketset | Mutual exclusion algorithm based on tickets using sets |
Safety Verification for Sequential Programs
The sequential examples for safety verification include:
- An implementation of skiplists with an unbounded number of levels. More information regarding this example can be found on this paper.
- A skiplist implementation which is part of the open-source project KDE.
- A bunch of examples dealing with skiplists of a fixed number of levels. More information about this example can be found on this paper
| title | description |
|---|---|
| skiplist | Skiplists of unbounded number of levels |
| skiplist-kde | Skiplist implementation from the open-source project KDE |
| skiplist_1 | Skiplists of at most 1 level |
| skiplist_2 | Skiplists of at most 2 levels |
| skiplist_3 | Skiplists of at most 3 levels |
| skiplist_4 | Skiplists of at most 4 levels |
| skiplist_5 | Skiplists of at most 5 levels |
Liveness Verification for Concurrent Programs
The concurrent examples for liveness verification include:
- A simple mutual exclusion algorithm based on tickets implemented with sets of integers.
| title | description |
|---|---|
| ticketset | Mutual exclusion algorithm based on tickets using sets |
| list | Concurrent lock-coupling lists |
All Examples
Alternatively, you can download all examples in a single zip file from here:
| title | description |
|---|---|
| all examples | All examples in a single zip file |