Verification 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
focus primarily on AtomicHashMap
(AHM) and AtomicHashArray
(AHA)
-
AtomicHashMap
-- claimed 2-5x faster thentbb::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
- get test suites compilable and runable under DIVINE (if it does not work start with custom/fake small test using
gtest/gtest.h
) - compile and load AHM/AHA tests to DIVINE (no verification yet, just check it loads)
- 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
- determine appropriate test sizes for minimal useful tests, parametrize tests for DIVINE appropriately
- 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 DIVINE