DIVINE issueshttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues2017-09-04T00:48:54+02:00https://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/32Run DIVINE over Julia test suite2017-09-04T00:48:54+02:00Vladimír ŠtillRun DIVINE over Julia test suitehttps://samate.nist.gov/SARD/testsuites/juliet/Juliet_Test_Suite_v1.2_for_C_Cpp.zip#https://samate.nist.gov/SARD/testsuites/juliet/Juliet_Test_Suite_v1.2_for_C_Cpp.zip#https://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/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/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 outFuture