Revert "spinlock model: Simplify state-space"

This reverts commit a9227ee907160443d0e4b1639b274ab9278d92fa.

Need to study impact on progress.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

Revert "Style Cleanup"

This reverts commit 03126291913d3c2df1d92137cf82767d9b490ade.

Need to study impact on progress.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

Revert "ticketlock model: state-space simplication"

This reverts commit d149fa02aaafa08c2d02712afd3cbbbc5f8d5f67.

Need to study impact on progress.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

ticketlock model: state-space simplication

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

Style Cleanup

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

spinlock model: Simplify state-space

Remove useless busy-looping, useless in Promela. Same semantic as the
new code:

Quoting Michel Dagenais <michel.dagenais@polymtl.ca>:

> http://spinroot.com/spin/Man/condition.html
> In Promela , a standalone expression is a valid statement. Execution
> of a condition statement is blocked until the expression evaluates to
> a non-zero value (or, equivalently, to the boolean value true ).
>
> http://spinroot.com/spin/Man/separators.html
> The semicolon and the arrow are equivalent statement separators in
> Promela. The convention is to reserve the use of the arrow separator
> to follow condition statements. The arrow symbol can thus be used to
> visually identify those points in the code where execution could
> block.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

Add back urcu QSBR selective wakeup model

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

Add 1ton readonly waiter model

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

1to1 selective wakeup: add misorder injection test

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

Update nto1 selective model

The nto1 selective wakeup model introduced by Paolo was:

a) too complex (tried to model the full-blown RCU rather than a simple
   queue system)
b) did not model progress with wakers running for a limited amount of
   iterations, only with wakers running infinitely often (which
   therefore does not prove anything).

What we really want to model here is what happens if we have wakers
running a few times, and then not running for a very long time: can we
end up with a missed wakeup, and therefore end up with an enqueued entry
but with the waiter waiting forever ?

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

update comment

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

Update nto1-selective model comments

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

Add nto1 futex wakeup scheme model

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

Move futex wakeup model to nto1-selective

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

futex model: Add futex_progress_inverted_waiting_vs_gp_futex error injection

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

model optimization of the waker (selective wake)

This patch adds to the model an optimization, whereby threads are
told whether they are still being waited on, and skip the futex wakeup
if not.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

new futex model

Rewrite the model to include the futex primitives and the list
move algorithm used by urcu.  The model implements a full-blown
parity-flipping RCU where grace period waits are driven exclusively
by futexes.  It runs the waker and waiter infinitely, asserting
that progress states (parity flips) are reached infinite times.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

update

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

better lock-free test

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

check wait free

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

update

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

update

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

add ticketlock test for wait-free (failed, as expected)

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

update gitignore

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Move formal-model to root

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Remove headers from formal model

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

only keep formal model

Update formal model from local copy

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Remove ifndef for API_H

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Add build support for ppc when $HOSTTYPE is "ppc"

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Separate arch_uatomic*.h from arch*.h

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Update tests api*.h

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Align registry data on cache line size

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

define CACHE_LINE_SIZE in arch_*.h

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

compiler.h: use stddef.h for offsetof

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Update .gitignore

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

urcu-qsbr: implement list_move algorithm

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

urcu (mb/signal): fix list move implementation

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

urcu (mb/signal): list move

Do no wait after a single thread at a time. When threads are Q.S., move them to
a separate list.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

list.h: add list_move

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

urcu (signal): export urcu_init for early constructor initialization

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

urcu-defer: use list instead of array for registry

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

urcu-qsbr: Add list sanity check at lib exit

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

urcu-qsbr: use linked list instead of array for registry

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

urcu (signal/mb): move thread checks outside lock

Done on local variables, no need to lock.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

urcu (signal/mb): use linked list instead of array for registry.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Update list, rculist and hlist

- rculist : license ok
- list : fix list del

Fix rcutorture api.h implementations to use non-GPL lists.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Add urcu list and list

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Cleanup headers

* atomic_ -> uatomic (to remove namespace clash with libkcompat)
* moved arch.h, compiler.h, arch_uatomic.h to
  /usr/include/urcu/

to make sure we do not pollute system headers.

Also add call_rcu() documentation to README.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Add missing urcu-defer.{so,h} and urcu-defer-static.h

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Document call_rcu() usage

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Add missing rcu_cmpxchg_pointer define

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Add multiple reader queues to futex model

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Cleanup promela code for wakeup verif

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Remove stale file

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Add multicoreverif paper ticketlock and spinlock models

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Add futex wakeup spin model

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Add futex support to accelerate synchronize_rcu() on UP

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

urcu-defer: fix futex wakeup value

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Remove extra LDFLAGS from makefile

> cc: -lpthread: linker input file unused because linking not done

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Add missing include compiler.h

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

rcu torture and api.h: remove duplicated atomic primitives

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

test_atomic: test for byte/short atomic support

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

ppc atomic: fix atomic_dec/inc

Only require 1 arg.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

urcu-defer: remove dependency on linux/futex.h

> cc -fPIC -Wall -I. -O2 -g -lpthread -c -o urcu-defer.o `echo urcu-defer.c urcu-defer.h | sed 's/[^ ]*\.h//g'`
> In file included from urcu-defer.c:31:
> /usr/include/linux/futex.h:96: error: expected ‘)’ before ‘*’ token
> /usr/include/linux/futex.h:100: error: expected ‘)’ before ‘*’ token

Seems broken on ppc. Just for two defines, it's not worth depending on it.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

urcu: Move urcu_init within ifdef

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

atomic ppc: fix missing casts and inline

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

urcu-defer: ensure callbacks will never be enqueued forever

Even if there are no further callbacks enqueued, ensure that after a 100ms
delay, the callback queue will be dealt with.

Required proper ordering of queue vs futex.

e.g.

 The idea is to perform the "check for empty queue" between the
&defer_thread_futex decrement and the test in wait_defer. It skips the
futex call and proceed if the list is non-empty.

As I am drilling into the problem, it looks very much like an attempt to
implement efficient wait queues in userspace based on sys_futex().

/*
 * Wake-up any waiting defer thread. Called from many concurrent
 * threads.
 */
static void wake_up_defer(void)
{
        if (unlikely(atomic_read(&defer_thread_futex) == -1)) {
                atomic_set(&defer_thread_futex, 0);
                futex(&defer_thread_futex, FUTEX_WAKE, 0,
                      NULL, NULL, 0);
        }
}

/*
 * Defer thread waiting. Single thread.
 */
static void wait_defer(void)
{
        atomic_dec(&defer_thread_futex);
        smp_mb();       /* Write futex before read queue */
        if (rcu_defer_num_callbacks()) {
                smp_mb();       /* Read queue before write futex */
                /* Callbacks are queued, don't wait. */
                atomic_set(&defer_thread_futex, 0);
        } else {
                smp_rmb();      /* Read queue before read futex */
                if (atomic_read(&defer_thread_futex) == -1)
                        futex(&defer_thread_futex, FUTEX_WAIT, -1,
                              NULL, NULL, 0);
        }
}

- call_rcu():
  * queue callbacks to perform
  * smp_mb()
  * wake_up_defer()

- defer thread:
  * for (;;)
    * wait_defer()
    * sleep 100ms (wait for more callbacks to be enqueued)
    * dequeue callbacks, execute them

The goal here is that if call_rcu() enqueues a callback (even if it
races with defer thread going to sleep), there should not be a
potentially infinite delay before it gets executed. Therefore, being
blocked in sys_futex while there is a callback to execute, without any
hope to be woken up unless another callback is queued, would not meet
that design requirement. I think that checking the number of queued
callbacks within wait_defer() as I propose here should address this
situation.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Fix urcu-defer: add missing brackets.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Cleanup: remove debug code form urcu-defer.c

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Move urcu_defer_queue to urcu-defer.c

Too big to be inline.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

urcu-defer: make call_rcu() energy efficient using futex()

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Add offsetof to compiler.h

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

ppc atomic: Fix asm format.

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

add rcu_cmpxchg_pointer

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

remove volatile from prototypes in atomic code

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

update ppc atomic

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

update x86 and ppc atomic ops

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Add powerpc atomic operations

cmpxchg
atomic_add_return
atomic_sub_return
atomic_add
atomic_sub
atomic_inc
atomic_dec

(already had xchg)

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

update x86_64 cmpxchg

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Update atomic x86_64 cmpxchg

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

makefile update

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Add inc/dec x86 atomics

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

update x86 atomic, add test atomic

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

extend x86 atomic operations

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Add missing files in make clean

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

urcu-defer: remove unnecessary memory barrier

All synchronization between queue producer/consumer is performed by the write to
"head". Before this write, none of the queued data is visible from the consumer
point of view.

Therefore, just a single wmb() is required before writing to head to ensure
correct synchronization. This matches with the rmb() after reading head on the
consumer side.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

urcu-defer: Add fast path for empty queues

defer_barrier does not need to call synchronize_rcu() when all queues are empty.
Skip the G.P. if this is the case.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

urcu-defer: cleanup debug code

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Deferral test update

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

generic urcu deferral (call_rcu())

Found out a way to encode the queues so the standard scenario is to use a single
pointer per call_rcu().

Uses more space for:
- unaligned functions pointers.
- unaligned data pointers.
- function/data value : -2L. (this is arbitrary)

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Rename liburcu-reclaim to liburcu-defer

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

urcu-reclaim cleanup

Rename "reader" to "reclaimer", because urcu-reclaim keeps track of "reclaimer"
threads (rcu writers) and has its own reclaiming thread periodically performing
the batch reclamation.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Update header heading

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Add rcu-reclaim.so library

Add "automated" RCU memory reclamation.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

add static declarations

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

qsbr: Add write+read thread support to 32-bit QSBR

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

QSBR: Implement 2-phase grace period for 32-bit arch

Ensures we never run in overflow on 32-bit arch.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Permit both 32 and 64-bit builds

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

Default to architecture size, add Makefile32

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>