projects
/
model-checker-benchmarks.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
The CDSSpec checker's benchmarks
[model-checker-benchmarks.git]
/
concurrent-hashmap
/
note.txt
diff --git
a/concurrent-hashmap/note.txt
b/concurrent-hashmap/note.txt
index 0056dcdc89fe1d2f1b9ef8907fd46957fc2d26dd..f080a487b1ac8fd614dbafd071e060220e3c0450 100644
(file)
--- a/
concurrent-hashmap/note.txt
+++ b/
concurrent-hashmap/note.txt
@@
-8,3
+8,10
@@
get(k2); // b get(k1); // d
When b and d both read the old head of the list (and they later grab the lock,
making it the interface SC), it's non-SC because neither reads the updated
value.
When b and d both read the old head of the list (and they later grab the lock,
making it the interface SC), it's non-SC because neither reads the updated
value.
+
+Run testcase1 to make the store and load of value slot to be seq_cst.
+
+Then run testcase2 with "-o annotation" to get store and load of key slot to be
+release/acquire.
+
+0m0.015s + 0m0.000 = 0m0.015s