Skip to content

GitLab

D
DIVINE
Open
Opened by Vladimír Štill@xstillOwner

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 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)
  3. 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
  4. determine appropriate test sizes for minimal useful tests, parametrize tests for DIVINE appropriately
  5. 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