edits: add comments to demonstrate the found bugs and bug injections

The CDSSpec checker's benchmarks

fix commit that mistakenly happened

fix compile errors on OS X

raw elimination-backoff code from paper

changes

add concurrent hashmap

Description of benchmarks

make warnings go away

clean up

add treiber stack

save fixed ms-queue

add cliff click hashtable

add result file

add seqlock

run.sh: sync up with model-checker improvements

remove unused benchmarks

These benchmakrs are hard to support, and at least one of them isn't
even supported by my g++ draft C++0x compiler (it tries to use structs
with bitfields in an atomic<> template).

run.sh: set Mac OSX DYLD_LIBRARY_PATH

DYLD_LIBRARY_PATH is the Mac OSX equivalent of Unix LD_LIBRARY_PATH.

bench.sh: only print git information when we're in git

Makefiles: use appropriate preprocessor vs. compiler flags

We should differentiate preprocessor vs. C++ compiler vs. C compiler
flags, according to the CPPFLAGS, CXXFLAGS, and CFLAGS conventions. That
way we can, for instance, easily add the appropriate --std=XXX flags
necessary for compiling with a C++11 (or C++0x) or C11 (or C1x)
compliant compiler.

Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker-benchmarks

chase-lev-dequeue: fix compiler warning

Fix this warning, found when compiling with GCC's C1x support:

  main.c: In function ‘task’:
  main.c:17:2: warning: implicit declaration of function ‘steal’ [-Wimplicit-function-declaration]

Makefile: compile the chase-leve deque bugfix

bugfix for chase lev

bench.sh: don't automatically log to file

Just print to STDOUT, and the user can manually pipe to a file if they
want.

bench.sh: rearrange order again

bench.sh: run dekker-fences

bench.sh: fixup Brian D.'s script change

Remove some duplicates; probably just a bad merge.

Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker-benchmarks

Conflicts:
bench.sh

my changes to benchmark shell

bench.sh: rewrite benchmark list to match paper

Brian D. changed the benchmarks we run as well as the order. Let's
encode that in this script, so we can repeat the benchmarks
consistently.

mpmc-queue: add to .gitignore

optimizations to mpmc-queue yield placement
simpler test case for concurrent readers/writers of mpmc-queue

Fix all benchmarks to use yield

All benchmarks now call thrd_yield when appropriate so that they terminate with the -y option.

deque: add .gitignore

ms-queue: add extra POISON_IDX assertion

ms-queue: finally, the correct (?) memory orderings

With much discussion over the intent of the algorithm and the accuracy
of these orderings, we have an accurate representation of the M&S Queue.

ms-queue: fixup initialization and free lists

There are a few things we fix:

1) We shouldn't initialize node[0].next, since node[0] is the 'NULL'
pointer and should never be accessed.

2) The per-thread free list is too restrictive. Now, we generate a list
of free nodes for each thread that can contain up to 4 node indexes.
We only initialize this list with 2 nodes each (so each thread can
expand its free list, if needed). There is some minimal assertion
framework and race detection performed on these lists, just in case.

3) We only initialize those nodes that are placed in the free list.
Accesses to other nodes' 'next' pointer should trigger an uninitialized
loads assertion.

ms-queue: don't initialize node 0

Node zero *should* be unused, since "0" is the NULL pointer index.
Removing this init will help catch bugs.

ms-queue: we should never dequeue 0

The test driver is written so that we should never dequeue 0.

ms-queue: revert Brian D. changes

On second (or third or fourth) thought, these changes were ill-advised.
We will make a different set of tweaks shortly.

This reverts commits 647601d3f341bb2a2a79534b3d044c039695839d and
fad3891f3158a4285984bb60415c1e4ebc2b767b.

wow...  i think this version is correct...

my changes

ms-queue: relax the second load of head/tail

ms-queue: strip down test driver

+ a few assertions

ms-queue: relax the queue loads/stores/CAS

Makefile: build ms-queue

deque: re-insert deleted MODEL_ASSERT()

deque: #include's

Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker-benchmarks

ms-queue: begin relaxing

Not functioning yet.

do merge...push right code
Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker-benchmarks

Conflicts:
chase-lev-deque/main.c

ms-queue: add initialization

deque: fix bugs in assertion code and move up 3 variables...

deque: add MODEL_ASSERT(), fixup #include's

deque: wrong bug fix before...now the correct one

deque: bug fix...method could return empty

deque: add test driver, add print messages for now for resize method and if we pull the wrong values

test case exposes model checker bugs :(

fix bug

ms-queue: relax the initializations

add make file, header, and extra code to deque

ms-queue: fixups, add simple race detection

ms-queue: bugfix - get_ptr() and get_count() were switched

I ported the implementation wrong, so that we were extracting bits from
the wrong field.

ms-queue: cleanups

ms-queue: remove more externs and unintended shared data

ms-queue: more cleanup

ms-queue: cleanups, convert to C11 atomics

This converts the "pointer" to a 64-bit type (unsigned long long, or
'pointer') divided into two 32-bit halves (ptr and count), instead of
using a union of a struct and an 'unsigned long'.

All atomics are seq_cst for now. Once the code all looks a little
better, I'll relax these to reasonable memory orderings.

mcs-queue -> ms-queue

This queue is by Michael and Scott; hence, "M&S".

mcs-queue: a few changes

mcs-queue: add Makefile

mcs-queue: modifications for compiling

Remove backoff, shmem, fork, etc.

Moving closer to something that can compile.

msc-queue: indentation, etc.

mcs-queue: initial checkin

The "new" queue (i.e., "MCS Queue") code directly from:

  ftp://ftp.cs.rochester.edu/pub/packages/sched_conscious_synch/concurrent_queues/concurrent_queues.tar.gz

Except for the MIPS assembly implementation files and Makefile.

From README:

The compressed tar file in this directory conatins the C code for
the algorithms implemented for the paper

%A Maged M. Michael
%A Michael L. Scott
%T Simple, Fast, and Practical Non-Blocking and Blocking
Concurrent Queue Algorithms
%J PROC of the Fifteenth PODC
%C Philadelphia, PA
%D May 1996
%X 23-26 May 1996
%K tr600
%O Earlier version available as
TR 600,
URCSD,
December 1995

deque: use atomic_uintptr_t

'Atomic(Array *)' seems to be a pseudocode type. Just use
atomic_uintptr_t and allow the warnings for now (we could alternatively
use a cast every time).

deque: improve compile-ability

Add appropriate C headers.
Re-introduce atomic_* and memory_order_* prefixes.

deque: add "proven correct" work-stealing Chase-Lev deque

From the PPoPP 2013 paper "Correct and efficient work-stealing for weak
memory models"

By:

  Nhat Minh Lê
  Antoniu Pop
  Albert Cohen
  Francesco Zappa Nardelli

Citation URL:

  http://dl.acm.org/citation.cfm?id=2442524

bench.sh: add dekker-fences to benchmark runs

bench.sh: log more information

We want the whole timing information and git-log info in our log files.

bench.sh: don't run tests twice

Now that we don't print so much garbage by default, we don't need to run
our tests twice (once with log and once without).

bench.sh: don't 'grep' output

Model-checker output is concise now, so don't trim it.

run.sh: sync up run script with model-checker

I improved the model-checker.git run script, so paste over the changes.

Makefile: build dekker-fences automatically

dekker-fences: add Dekker's critical section algorithm

Now that we support fences, add a test benchmark that uses fences. This
one just uses seq-cst fences.

Downloaded from:

   http://www.justsoftwaresolutions.co.uk/threading/

Modified to avoid static construction. i.e., change:
  std::atomic<int> turn(0);
to
  std::atomic<int> turn;
  ...
  turn = 0;
And added user_main() method to launch the two threads.

bench.sh: add spsc-bugfix to benchmark runs

Makefile: build spsc-bugfix by default

spsc-bugfix: fix deadlocked signalling bug

spsc-bugfree: make Relacy run exhaustive, fair scheduler

spsc-bugfix: duplicate the (buggy) spsc-queue

Preparing to fix the deadlock bug.

unrelacy: instrument relacy-marked normal loads/stores

bench: reconfigure default tests

Now, run the "-noinit" tests for mpmc-queue (2R2W and 1R2W). Also,
switch to using '-f 10 -m 2 -e 1' model-checking parameters.

mpmc-queue: .gitignore

mpmc-queue: add "-noinit" builds

Build matching test cases where there is no initial element in the
queue.

mpmc-queue: makefile bugfix

mpmc-queue: remove duplicate source files

mpmc-queue: unify source file again

I really didn't want 3 copies of the same source file just to get around
some model-checker snapshotting limitations in argument parsing... So
now, it's a compile-time option to configure the number of reader/writer
threads.

mpmc-queue: fix make clean

spsc-queue: add spsc-relacy build

Now we can test a version of spsc-queue using Relacy. There were some
small modifications necessary, so I duplicated the source code, renamed
with "-relacy" in the name.

To use it, you need to do something like the following, from the
spsc-queue directory:

  make RELACYPATH=/path-to-relacy
  ./spsc-relacy

unrelacy: include <mutex> and <condition_variable>

Relacy expects to have these headers even if they aren't included by the
program.

spsc-queue: fix some old Relacy syntax (RL_NEW/RL_DELETE)

Relacy 2.4 doesn't even have RL_NEW and RL_DELETE, so we shouldn't use
it even if we're trying to be Relacy-compatible.

unrelacy: use new MODEL_ASSERT() macro