DIVINE issueshttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues2017-09-04T00:48:53+02:00https://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/39Add missing POSIX features2017-09-04T00:48:53+02:00Jiří WeiserAdd missing POSIX features* Add file `sys/param.h`.
* Add error code `ENOTSUP`.
* Add scheduler policy constants `SCHED_OTHER`, `SCHED_FIFO`, and `SCHED_RR`.
* Make `PTHREAD_INHERIT_SCHED` and `PTHREAD_EXPLICIT_SCHED` expand to different values.
* Make `PTHREAD_S...* Add file `sys/param.h`.
* Add error code `ENOTSUP`.
* Add scheduler policy constants `SCHED_OTHER`, `SCHED_FIFO`, and `SCHED_RR`.
* Make `PTHREAD_INHERIT_SCHED` and `PTHREAD_EXPLICIT_SCHED` expand to different values.
* Make `PTHREAD_SCOPE_PROCESS` and `PTHREAD_SCOPE_SYSTEM` expand to different values.
* Add definitions for signals
* `struct sigaction`
* `sigfillset`
* `sigaction`
* `SIGUSR1`, `SIGUSR2`, `SIGALARM`Futurehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/36create VM images for all historical versions of DIVINE2017-09-04T00:48:53+02:00Petr Ročkaicreate VM images for all historical versions of DIVINE* each version gets its own VM image (there may be mutually incompatible dependencies)
* for cluster (MPI-enabled) versions, it should be possible to spin up multiple copies of an image and have them run a distributed job
* main motiva...* each version gets its own VM image (there may be mutually incompatible dependencies)
* for cluster (MPI-enabled) versions, it should be possible to spin up multiple copies of an image and have them run a distributed job
* main motivation is to improve benchmarking reproducibility and ease comparisons
* documentation
* Bc. thesisFuturehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/29Verification of boost's concurrent data structures2017-09-04T00:48:54+02:00Vladimír ŠtillVerification of boost's concurrent data structuresThe aim of this task is to verify two parallel structures of Boost - lock-
free queue and lock-free stack. The task could be divided into few
subtasks:
1. Compile DIVINE
2. Read the paper
(http://www.cs.rochester.edu/~scott/pap...The aim of this task is to verify two parallel structures of Boost - lock-
free queue and lock-free stack. The task could be divided into few
subtasks:
1. Compile DIVINE
2. Read the paper
(http://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf)
3. Compile Boost library with dummy main
4. Specify and implement test-cases
5. Verify test-cases with DIVINE
6. Analyse results
7. Sumarize results and make a presentation.Futurehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/28Add support of usage glibc instead of PDCLib2017-09-04T00:48:54+02:00Vladimír ŠtillAdd support of usage glibc instead of PDCLibFuturehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/27Verification of lvmetad (LVM2's metadata caching daemon)2017-09-04T00:48:54+02:00Vladimír ŠtillVerification of lvmetad (LVM2's metadata caching daemon) - fairly self-contained code
- concurrency, dynamic memory
- daemon: driven by external requests on a socket interface - fairly self-contained code
- concurrency, dynamic memory
- daemon: driven by external requests on a socket interfaceFuturehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/26Verification of clvmd (LVM2's cluster locking & coordination daemon)2017-09-04T00:48:54+02:00Vladimír ŠtillVerification of clvmd (LVM2's cluster locking & coordination daemon) - old, complex codebase
- heavy use of pthread primitives (mutexes, condition variables)
- links to LVM code, with lots of system interaction that would need to be
stubbed out or otherwise 'neutralised'
- talks to kernel's DLM (... - old, complex codebase
- heavy use of pthread primitives (mutexes, condition variables)
- links to LVM code, with lots of system interaction that would need to be
stubbed out or otherwise 'neutralised'
- talks to kernel's DLM (distributed lock manager), but this layer is
modular and could be replacedFuturehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/25Verification of lvmlockd (LVM2's new distributed locking daemon)2017-09-04T00:48:54+02:00Vladimír ŠtillVerification of lvmlockd (LVM2's new distributed locking daemon) - modern replacement for clvmd (cf. #26)
- sanlock-based and dlm-based locking
- socket communication, based on same library as lvmetad (cf. #27)
- verification: besides internal threading and access to data structures,
interact... - modern replacement for clvmd (cf. #26)
- sanlock-based and dlm-based locking
- socket communication, based on same library as lvmetad (cf. #27)
- verification: besides internal threading and access to data structures,
interaction of multiple lvmlockd instances (probably needs implementing a
'fake' locking mechanism, other than existing sanlock+dlm; would be also
useful in testing)Futurehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/24Visualization of heap of program/counterexample2018-07-07T03:15:48+02:00Vladimír ŠtillVisualization of heap of program/counterexampleDIVINE 4 already has graph memory, so turning it into visualization e.g. using DOT should be possible. However, the challenge is in presentation: it would be useful to have nodes labeled with types and pointers with member/variable names...DIVINE 4 already has graph memory, so turning it into visualization e.g. using DOT should be possible. However, the challenge is in presentation: it would be useful to have nodes labeled with types and pointers with member/variable names they represent. Also it would be useful to be able to show only parts of the heap, e.g. corresponding to one thread, omitting DiOS,…Futurehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/19Probabilistic extension for data-symbolic verification2016-06-19T13:04:15+02:00Jiří BarnatProbabilistic extension for data-symbolic verificationWaiting for #20, #21, #22.Waiting for #20, #21, #22.Futurehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/18Objective C/C++ verification with DIVINE2016-06-19T12:47:27+02:00Jiří BarnatObjective C/C++ verification with DIVINEThe goal of the project is to explore the possibilities of verification of Objective C/C++ through clang native support of these programming languages.The goal of the project is to explore the possibilities of verification of Objective C/C++ through clang native support of these programming languages.Futurehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/17Syscall record and replay.2016-06-17T10:22:40+02:00Vladimír ŠtillSyscall record and replay.Allow divine run to call syscalls, record them and then allow to replay them.Allow divine run to call syscalls, record them and then allow to replay them.Futurehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/16Verification of Folly.2016-07-08T10:17:13+02:00Vladimír ŠtillVerification of Folly.<https://github.com/facebook/folly>
Namely of AtomicHashArray/AtomicHashMap and other Atomic* primitives.
See https://github.com/facebook/folly/blob/master/folly/docs/Overview.md
## Headers containing parallel primitives
focu...<https://github.com/facebook/folly>
Namely of AtomicHashArray/AtomicHashMap and other Atomic* primitives.
See https://github.com/facebook/folly/blob/master/folly/docs/Overview.md
## Headers containing parallel primitives
focus primarily on `AtomicHashMap` (AHM) and `AtomicHashArray` (AHA)
* `AtomicHashMap` -- claimed 2-5x faster then `tbb::concurrent_hash_map`, manages growth poorly
* `AtomicHashArray` -- building block of AHM
* `AtomicLinkedList`
* `ThreadCachedArena`
* `Baton` - kind of one-time semaphore/barrier/latch
* `ConcurrentSkipList`
* `RWSplinLock`, `SmallLocks` -- probably trivial
* `ThreadChachedInt`
* `futures/*`
furthermore, probably much more complex:
* `fibers/*`
## Subasignments for verification
1. get test suites compilable and runable under DIVINE (if it does not work start with custom/fake small test using `gtest/gtest.h`)
2. compile and load AHM/AHA tests to DIVINE (no verification yet, just check it loads)
2. analyze tests for AHM/AHA for size and complexity sources, parametrization, add parameters (preferably using defaulted templates) to make it possible to control test size
3. determine appropriate test sizes for minimal useful tests, parametrize tests for DIVINE appropriately
4. run tests in DIVINE
## What should be written
* describe the data structures, their desing
* compare design of AHM with DIVINE's own parallel hash table (ref. brick-hashset, https://link.springer.com/chapter/10.1007/978-3-319-23404-5_5)
* compare performace of AHM with DIVINE's parallel hash table
* optionally: integrate AHM into DIVINE 3 and compare performance in DIVINEFuturehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/14Parametrized-Precision Verification for C/C++.2016-06-19T13:47:23+02:00Vladimír ŠtillParametrized-Precision Verification for C/C++.Often especially if the model is large it would be useful to a add assumptions about the environment such as:
* allocation does not fail
* threading primitives are bug-free and "as atomic as possible" i.e. thread starting does not in...Often especially if the model is large it would be useful to a add assumptions about the environment such as:
* allocation does not fail
* threading primitives are bug-free and "as atomic as possible" i.e. thread starting does not interleave `std::thread` constructor with the new thread until the user-provided thread entry function is ready to run, `std::mutex::lock` is atomic,…
* exception throwing and catching is atomic
* …
This should be done by annotating the libraries with conditional mask points which would be activated probably by LART pass in loader.
The work also includes benchmarking impact of these reductions on the state space size.Futurehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/13Verification of NSCD (glibc's name serice cache daemon)2016-07-04T15:57:40+02:00Vladimír ŠtillVerification of NSCD (glibc's name serice cache daemon) - tied into glibc code (cf. #28)
- partially verified, cf. the master thesis of Milan Lenčo <https://is.muni.cz/auth/th/359883/fi_m/>
- sockets, dynamic memory, interaction with clients - tied into glibc code (cf. #28)
- partially verified, cf. the master thesis of Milan Lenčo <https://is.muni.cz/auth/th/359883/fi_m/>
- sockets, dynamic memory, interaction with clientsFuturehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/12Verification of Hazard Pointers.2016-06-16T21:54:16+02:00Vladimír ŠtillVerification of Hazard Pointers.Futurehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/11Verification of Intel TBB concurrent data structures2016-07-04T15:50:39+02:00Vladimír ŠtillVerification of Intel TBB concurrent data structures - complex C++ code base
- very complex memory management
- straightforward verification, after memory management is sorted out - complex C++ code base
- very complex memory management
- straightforward verification, after memory management is sorted outFuturehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/10Support for WIN32 threads.2016-08-15T22:23:12+02:00Vladimír ŠtillSupport for WIN32 threads.Low priority.Low priority.Futurehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/9LART: Register allocation.2016-06-17T10:24:30+02:00Vladimír ŠtillLART: Register allocation.FutureVladimír ŠtillVladimír Štillhttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/8Partial Order for LLVM.2016-06-16T21:55:38+02:00Vladimír ŠtillPartial Order for LLVM.Although Tau reduction is in a way POR.Although Tau reduction is in a way POR.Futurehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/7Timed LLVM & UppAll to LLVM.2016-06-16T21:58:05+02:00Vladimír ŠtillTimed LLVM & UppAll to LLVM.Future