#1 Some metrics to show how difficult to write specifications for the benchmarks. ELOC --- Essential Lines of Code (Without counting blanks and comments) LOES --- Lines of Essential Specificaitons (Without counting the "/** @Begin" and "@End */") SDS --- Sequential Data Structure OP --- Ordering Points PS --- Pre/post-conditions and SideEffects Benchmark ELOC #API methods #OP LOES for SDS LOES for PS LOES for OP LOES for Synchronization total LOES LOES (OP + Sync) Chase-Lev Deque 92 3 5 27 19 13 6 65 19 SPSC Queue 129 2 2 27 7 6 3 43 9 ReadCopyUpdate 26 2 2 3 5 6 3 17 9 Lockfree Hashtable 421 2 4 44 11 22 5 82 27 MCS Lock 151 2 4 3 6 10 1 20 11 MPMC Queue 65 4 8 0 0 32 5 37 37 M&S Queue 59 2 6 27 10 22 3 62 25 Linux RW Lock 90 6 11 6 21 28 10 65 38 Total 1033 23 42 137 79 139 36 391 175