userspace-rcu.git
15 years agoModel used for ipi verification run #1
Mathieu Desnoyers [Sat, 30 May 2009 22:30:30 +0000 (18:30 -0400)] 
Model used for ipi verification run #1

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoConfiguration for remote barrier formal verif run
Mathieu Desnoyers [Fri, 29 May 2009 14:59:29 +0000 (10:59 -0400)] 
Configuration for remote barrier formal verif run

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoUpdate spin model
Mathieu Desnoyers [Thu, 28 May 2009 13:40:48 +0000 (09:40 -0400)] 
Update spin model

- Add memory poisoning to the ooo insn sched section.
- Put pointer update into ooo insn sched section.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoUse define SLAB_SIZE in promela model
Mathieu Desnoyers [Wed, 27 May 2009 14:38:27 +0000 (10:38 -0400)] 
Use define SLAB_SIZE in promela model

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agourcu model wmb/read barrier depend
Mathieu Desnoyers [Wed, 27 May 2009 03:43:46 +0000 (23:43 -0400)] 
urcu model wmb/read barrier depend

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd .gitignore entries to reduce 'git status' chatter
Paul E. McKenney [Wed, 27 May 2009 01:03:24 +0000 (21:03 -0400)] 
Add .gitignore entries to reduce 'git status' chatter

Add some entries to .gitignore files to reduce chatter from "git status".

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agocatch urcu-paulmck.spin to my local version
Paul E. McKenney [Tue, 26 May 2009 17:35:53 +0000 (13:35 -0400)] 
catch urcu-paulmck.spin to my local version

The attached patch catches the repository up to my local version.
This adds the following:

o       Checking for no-progress cycles.

o       Allow enabling and disabling of update-side signal-mediated
        broadcast memory barriers via #define statements.

o       Enabling only those update-side signal-mediated broadcast
        memory barriers that are required for correctness.

This version assumes that synchronize_rcu() is locally ordered, for
example, with smp_mb() calls between each pair of major statements.
Please note that smp_mb() is -not- assumed within the loops nor
immediately before the second counter flip.

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agosync_core to smp_mb transition
Mathieu Desnoyers [Tue, 26 May 2009 17:31:36 +0000 (13:31 -0400)] 
sync_core to smp_mb transition

- move sync_core to smp_mb in urcu.c, update comments.
- cpuid clashes with -fPIC because it clobbers ebx. Use mb() if ___PIC__ is
  defined.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoFix standard (no remote barrier) parity flip bug
Mathieu Desnoyers [Wed, 20 May 2009 17:02:22 +0000 (13:02 -0400)] 
Fix standard (no remote barrier) parity flip bug

A bug was introduced when moving from statically assigning the parity to wait
for on the update side (first even, then odd) to a model trying to deal the
single flip test case. It occurs that when busy-looping, the parity flip
occurred when it should not.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoSpecial-case reader/writer busy-loop for signals in progress
Mathieu Desnoyers [Wed, 20 May 2009 14:53:55 +0000 (10:53 -0400)] 
Special-case reader/writer busy-loop for signals in progress

The reader may choose to always ignore signal requests or to busy-loop always
waiting for signal requests. Those are much less interesting wrt progress. Add
progress statements in those loops.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoFix single flip test
Mathieu Desnoyers [Wed, 20 May 2009 13:01:06 +0000 (09:01 -0400)] 
Fix single flip test

The single flip test requires to keep track of parity evolution across the loop
iterations. Keep it as a local variable so we don't end up adding unexisting
dependencies.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoFix urcu controldataflow model remote barriers
Mathieu Desnoyers [Wed, 20 May 2009 04:25:17 +0000 (00:25 -0400)] 
Fix urcu controldataflow model remote barriers

Need to split the pointer read from the data access to allow the writer to issue
a memory barrier (actually more than one) to let the single flip race occur.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoDocument update in urcu.spin header
Mathieu Desnoyers [Tue, 19 May 2009 22:11:12 +0000 (18:11 -0400)] 
Document update in urcu.spin header

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd extended urcu model with ooo mem and instruction scheduling
Mathieu Desnoyers [Tue, 19 May 2009 22:07:08 +0000 (18:07 -0400)] 
Add extended urcu model with ooo mem and instruction scheduling

Here is the new model I worked on for the past weeks. It models :

- out-of-order memory accesses.
- instruction scheduling by the CPU on the write and read sides.

The model as committed in the repository at

formal-model/urcu-controldataflow

models the urcu with memory barriers on the read-side. It works exactly
as expected. mb() on the read-side is enabled when we have this in
the DEFINES file :

//#define REMOTE_BARRIERS   (commented out)

To run all tests, just fire :

make
(with spin 5.1.7 here. 5.2.0 has a bug with arrays of size 1)

Verification summary
asserts.log:State-vector 64 byte, depth reached 2801, errors: 0
urcu_free.log:State-vector 88 byte, depth reached 3302, errors: 0
urcu_free_no_mb.log:State-vector 88 byte, depth reached 24407, errors: 1
urcu_free_single_flip.log:State-vector 88 byte, depth reached 2904, errors: 1
urcu_progress_reader.log:State-vector 80 byte, depth reached 3353, errors: 0
urcu_progress_writer_error.log:State-vector 80 byte, depth reached 8035, errors: 1
urcu_progress_writer.log:State-vector 80 byte, depth reached 3348, errors: 0

However, I still have a problem modeling the signal-based barriers.

(remove comment from the define)

make urcu_free_single_flip should generate an error (just like it does
with the reader-mb() case), but it does not. I think it's caused by
added serialization due to the writer waiting on the reader barriers.

Normally, this model should behave similarly to yours : it should honor
the barrier requests before each read-side instruction IIF the
instruction execution order is in program order.

I'm pretty sure I missed something obvious, but I think it's time I
share the model I have with you so you might help me spot what I missed.
It may be as simple as an incorrect instruction scheduling dependency
too.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoSupport gcc which does not support constructor attribute
Mathieu Desnoyers [Tue, 19 May 2009 17:37:03 +0000 (13:37 -0400)] 
Support gcc which does not support constructor attribute

- Add call to urcu_init from reader thread registration.
- Try to move the constructor and destructor attribute to the prototype, in case
  gcc has problems with these attributes used with the function definition.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoFix opensuse powerpc build
Steven Munroe [Tue, 19 May 2009 17:14:53 +0000 (13:14 -0400)] 
Fix opensuse powerpc build

I gave this code a spin on a G5 (PPC970) OpenSuse 10.3 system and
encountered same issues that should fix fot tyou next update.

The liburcu make system sis not set up for biarch (32-/64-bit) builds on
PPC. SLES10/OpenSUSE-10.3 is a default 32-bit, 64-bit capable system. To
build a 64-bit you need to insert -m64 for all compiles and link
operations. Also for 64-bit make install should move liburcu.so
to /usr/lib64 not /usr/lib. This is required to FSB complience. Is
worked around this by copying Makefile to Makefile64 and made the
required changes there.

For SLES11 we changed to to a 64-bit default and 32-bit capable system.
In either case you need to be able to build both 32-/64-bit liburcu.so
on same systems and need to insure that make install is appropriate.

Also I found that __SIZEOF_LONG__ was not defined and resulted in a
sigill on PPC64. I suspect this is XLC specific and you need solution
that works for GCC builds as well.

I have attached a patch that implement these change for your review.
With this patch I can build liburcu and run the tests successfully.

Finally when I build 32-bit (default for OpenSUSE 10) I get a unhandled
SIGUSER1. I ran out of weekend before I could figure that out.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoDocument thread registration in urcu.h
Mathieu Desnoyers [Sat, 16 May 2009 21:27:06 +0000 (17:27 -0400)] 
Document thread registration in urcu.h

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoDocument rcu_register_thread in README
Mathieu Desnoyers [Sat, 16 May 2009 21:25:18 +0000 (17:25 -0400)] 
Document rcu_register_thread in README

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoUpdate ooo mem model comments
Mathieu Desnoyers [Fri, 15 May 2009 22:35:40 +0000 (18:35 -0400)] 
Update ooo mem model comments

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoRemove old memory models
Mathieu Desnoyers [Fri, 15 May 2009 20:35:57 +0000 (16:35 -0400)] 
Remove old memory models

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoUpdate out of order memory models to include instruction scheduling
Mathieu Desnoyers [Fri, 15 May 2009 20:31:18 +0000 (16:31 -0400)] 
Update out of order memory models to include instruction scheduling

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoMove reader barrier within if statement for outermost nesting
Mathieu Desnoyers [Fri, 15 May 2009 02:09:24 +0000 (22:09 -0400)] 
Move reader barrier within if statement for outermost nesting

Innermost nesting levels do not need this barrier. Slight runtime cost when
compiling with reader barriers in place. Does not change anything when using the
signal-based scheme.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoUse sync_core() in the write side to match current formal verif model
Mathieu Desnoyers [Wed, 13 May 2009 18:09:34 +0000 (14:09 -0400)] 
Use sync_core() in the write side to match current formal verif model

The formal model we currently have assumes serialized instruction execution on
the write-side. Until we extend this model to allow out-of-order instruction
execution, add equivalent synchronization in the library code.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoadd sync_core primitive
Mathieu Desnoyers [Wed, 13 May 2009 18:03:52 +0000 (14:03 -0400)] 
add sync_core primitive

Add sync_core() to serialize instruction execution on a core.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd rewrite of rep_nop
Mathieu Desnoyers [Wed, 13 May 2009 17:40:26 +0000 (13:40 -0400)] 
Add rewrite of rep_nop

Rewritten from scratch, OK for LGPL license.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoRemove rep_nop() (GPL)
Mathieu Desnoyers [Wed, 13 May 2009 17:38:50 +0000 (13:38 -0400)] 
Remove rep_nop() (GPL)

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoLGPLv2.1 relicensing statement
Mathieu Desnoyers [Wed, 13 May 2009 15:21:26 +0000 (11:21 -0400)] 
LGPLv2.1 relicensing statement

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoApply MIT-style license to compiler.h
Mathieu Desnoyers [Wed, 13 May 2009 15:21:02 +0000 (11:21 -0400)] 
Apply MIT-style license to compiler.h

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoRewrite of likely, unlikely, barrier and ACCESS_ONCE
Mathieu Desnoyers [Wed, 13 May 2009 15:15:37 +0000 (11:15 -0400)] 
Rewrite of likely, unlikely, barrier and ACCESS_ONCE

compiler.h now licensed under MIT-style license.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoRemoving GPL likely, unlikely, ACCESS_ONCE and barrier
Mathieu Desnoyers [Wed, 13 May 2009 15:09:49 +0000 (11:09 -0400)] 
Removing GPL likely, unlikely, ACCESS_ONCE and barrier

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoCreate separate document for relicensing details
Mathieu Desnoyers [Wed, 13 May 2009 13:59:01 +0000 (09:59 -0400)] 
Create separate document for relicensing details

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoFix some typos in PowerPC support code.
Paul E. McKenney [Wed, 13 May 2009 03:43:01 +0000 (23:43 -0400)] 
Fix some typos in PowerPC support code.

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoRemove bogus comment.
Mathieu Desnoyers [Tue, 12 May 2009 19:31:55 +0000 (15:31 -0400)] 
Remove bogus comment.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoImplementation of xchg primitives derived from MIT license
Mathieu Desnoyers [Tue, 12 May 2009 19:28:55 +0000 (15:28 -0400)] 
Implementation of xchg primitives derived from MIT license

See LICENSE for details.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd Paul's URCU model
Mathieu Desnoyers [Mon, 11 May 2009 20:58:17 +0000 (16:58 -0400)] 
Add Paul's URCU model

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoFix arch_ppc precompiler error
Mathieu Desnoyers [Mon, 11 May 2009 02:53:36 +0000 (22:53 -0400)] 
Fix arch_ppc precompiler error

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoFix precompiler error in arch_*.h, add arch-api test
Mathieu Desnoyers [Mon, 11 May 2009 02:50:48 +0000 (22:50 -0400)] 
Fix precompiler error in arch_*.h, add arch-api test

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd final license to test file, cleanup makefile
Mathieu Desnoyers [Mon, 11 May 2009 02:24:24 +0000 (22:24 -0400)] 
Add final license to test file, cleanup makefile

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoRemove automatically generated api.h from repository
Mathieu Desnoyers [Mon, 11 May 2009 02:22:02 +0000 (22:22 -0400)] 
Remove automatically generated api.h from repository

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd missing urcu-static.h
Mathieu Desnoyers [Mon, 11 May 2009 02:20:47 +0000 (22:20 -0400)] 
Add missing urcu-static.h

This new file should be inly included in LGPL-compatible code.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoLGPL relicensing part 2
Mathieu Desnoyers [Mon, 11 May 2009 02:15:08 +0000 (22:15 -0400)] 
LGPL relicensing part 2

Rewrote the non-trivial functions in arch_ppc.h and arch_x86.h.

Added complete header license declarations. Created LICENSE file to explain the
library licence.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoLGPLv2.1 relicensing
Mathieu Desnoyers [Mon, 11 May 2009 00:54:43 +0000 (20:54 -0400)] 
LGPLv2.1 relicensing

Except the content of arch_x86.h and arch_ppc.h, everything that was not
LGPL-compatible has been either rewritten or was simply a trivial one-liner.

The only content which could still be non-LGPL licensable in this commit is :

arch_ppc.h: atomic_inc()
            __xchg_u32()
            get_cycles (maybe ?)

arch_x86.h: __xchg()

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd ACCESS_ONCE to _STORE_SHARED
Mathieu Desnoyers [Sat, 9 May 2009 14:48:38 +0000 (10:48 -0400)] 
Add ACCESS_ONCE to _STORE_SHARED

We assume that the compiler does not reorder _STORE_SHARED across each other
and wrt _READ_SHARED. We therefore need to mark this access as volatile. The
compiler cannot reorder volatile accesses.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoLGPL relicensing of IBM's contributions
Paul E. McKenney [Sat, 9 May 2009 05:11:49 +0000 (01:11 -0400)] 
LGPL relicensing of IBM's contributions

Add comments noting IBM's permission to relicense its contributions to the
urcu.h and urcu.c files under the LGPLv2 license, or any later version.

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Reviewed-by: Steven L. Bennett <steven.bennett@us.ibm.com>
15 years agoformal verif : move bits produced declarations closer to processes
Mathieu Desnoyers [Fri, 8 May 2009 19:54:54 +0000 (15:54 -0400)] 
formal verif : move bits produced declarations closer to processes

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd no sync_core() test to ooo two writes model
Mathieu Desnoyers [Fri, 8 May 2009 18:18:03 +0000 (14:18 -0400)] 
Add no sync_core() test to ooo two writes model

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd instruction scheduling model using SSA model
Mathieu Desnoyers [Fri, 8 May 2009 18:14:30 +0000 (14:14 -0400)] 
Add instruction scheduling model using SSA model

As promised, here is a new model :-) So far the results are very good.

Basically, I model the dependencies between the instructions using a SSA
assignment. It behaves a bit like a Petri network, passing tokens
between the "instructions". When instructions have multiple dependencies
as input, they wait for all their input tokens to be ready before they
execute. It assumes we have an infinite number of registers available to
hold the variables, given this is an "abstract" architecture.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd readme file
Mathieu Desnoyers [Fri, 8 May 2009 15:26:27 +0000 (11:26 -0400)] 
Add readme file

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoRemove arch.h
Mathieu Desnoyers [Fri, 8 May 2009 14:29:10 +0000 (10:29 -0400)] 
Remove arch.h

Created by build scripts.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd missing arch.h
Mathieu Desnoyers [Fri, 8 May 2009 14:21:10 +0000 (10:21 -0400)] 
Add missing arch.h

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd ooo mem instruction scheduling
Mathieu Desnoyers [Mon, 27 Apr 2009 20:19:17 +0000 (16:19 -0400)] 
Add ooo mem instruction scheduling

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoRemove unneeded signal in the cache-coherent case
Mathieu Desnoyers [Sun, 26 Apr 2009 23:13:58 +0000 (19:13 -0400)] 
Remove unneeded signal in the cache-coherent case

the "reader kick" signal is only needed to perform a smp_mc() on readers, which
is pointless in a cache-coherent arch.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoMinor fix to userspace-rcu Makefile
Paul E. McKenney [Tue, 21 Apr 2009 17:30:39 +0000 (13:30 -0400)] 
Minor fix to userspace-rcu Makefile

Small update to the Makefile to allow it to clean up more completely.

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoSupport kernels with broken signal delivery
Paul E. McKenney [Sat, 18 Apr 2009 06:43:32 +0000 (02:43 -0400)] 
Support kernels with broken signal delivery

Some Linux kernels seems to have problems sending _all_ the signals. Use a
workaround which re-sends the signal when we wait for it to be executed.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd x86 and ppc arch definitions
Paul E. McKenney [Sat, 18 Apr 2009 06:34:37 +0000 (02:34 -0400)] 
Add x86 and ppc arch definitions

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agochange reader_data for reader_registry
Mathieu Desnoyers [Sun, 12 Apr 2009 02:59:42 +0000 (22:59 -0400)] 
change reader_data for reader_registry

> > In Figure 9, "reader_data" shouldn't be used as both a variable name
> > and a structure tag.  Furthermore, the text needs to explain what it
> > is.
>
> I will defer to Mathieu on this one, though it would certainly prevent
> using this code in a C++ program.
>

Yes, I've been lazy on the naming here. How about :

struct reader_registry {
        pthread_t tid;
        long *urcu_active_readers;
};

static struct reader_registry *registry;

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoSplit out architecture-dependent definitions into api.h and arch.h.
Paul E. McKenney [Fri, 10 Apr 2009 16:41:19 +0000 (12:41 -0400)] 
Split out architecture-dependent definitions into api.h and arch.h.

Break out architecture-specific definitions into api.h and arch.h.
Modify Makefile to add pthreads-x86 and pthreads-ppc targets to adapt
to either architecture.  Create api_x86.h, api_ppc.h, arch_x86.h, and
arch_ppc.h files.

The api/arch distinction is historical in nature.  In a perfect world,
these would be merged.  In reality, the __thread storage class does not
adapt nicely to accessing one thread's variables from another thread,
though sufficiently insane gcc hackery could probably make this work.
In the event, arch.h manually constructs an array of pointers to the
__thread variables that need cross-thread access, while api.h punts
and uses an array for the per-thread variables themselves, paying a
significant performance penalty for so doing.

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoDon't mix pthread sleepable lock with busy-waiting locking.
Mathieu Desnoyers [Wed, 8 Apr 2009 00:35:46 +0000 (20:35 -0400)] 
Don't mix pthread sleepable lock with busy-waiting locking.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoUse more standard flags
Mathieu Desnoyers [Mon, 6 Apr 2009 20:41:20 +0000 (16:41 -0400)] 
Use more standard flags

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoCheck double write read order
Mathieu Desnoyers [Mon, 6 Apr 2009 20:30:04 +0000 (16:30 -0400)] 
Check double write read order

Check the following scenario :

> > P.S.:  Regarding very weak memory-ordering models, I recall that in our
> > earlier discussions we considered this scenario:

> >     CPU 0                   CPU 1
> >     -----                   -----
> >     x = 1;                  y = 1;
> >     mb();                   mb();
> >     read y                  read x

> > with the question being whether it was possible for both reads to
> > obtain the value 0.  With sufficiently weak ordering it is possible,
> > but it turned out that there are places in the Linux kernel (I don't
> > remember where) that essentially assume this cannot happen.  Have you
> > gotten far enough in your outline of the semi-formal model to address
> > this sort of question?

15 years agoCommit urcu verif results
Mathieu Desnoyers [Wed, 1 Apr 2009 02:01:30 +0000 (22:01 -0400)] 
Commit urcu verif results

Use make summary is each dir.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoCommit for tests
Mathieu Desnoyers [Wed, 1 Apr 2009 02:01:09 +0000 (22:01 -0400)] 
Commit for tests

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoExecute sig handler unconditionnally
Mathieu Desnoyers [Mon, 30 Mar 2009 20:52:46 +0000 (16:52 -0400)] 
Execute sig handler unconditionnally

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoRCU signal handler reader over reader
Mathieu Desnoyers [Sun, 29 Mar 2009 02:40:33 +0000 (22:40 -0400)] 
RCU signal handler reader over reader

Added RCU test for read over read signal handler.

Data structures can now support multiple readers, but it fills my system's
memory (16GB+).

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoremove duplicate ooo_mem statements
Mathieu Desnoyers [Thu, 19 Mar 2009 20:47:29 +0000 (16:47 -0400)] 
remove duplicate ooo_mem statements

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoadd missing ooo_mem() to writer model
Mathieu Desnoyers [Thu, 19 Mar 2009 19:13:12 +0000 (15:13 -0400)] 
add missing ooo_mem() to writer model

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agospin model : inline reader
compudj [Thu, 19 Mar 2009 18:05:02 +0000 (14:05 -0400)] 
spin model  : inline reader

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd documentation of urcu
compudj [Mon, 2 Mar 2009 16:15:54 +0000 (11:15 -0500)] 
Add documentation of urcu

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd remote barrier model
Mathieu Desnoyers [Fri, 27 Feb 2009 19:13:12 +0000 (14:13 -0500)] 
Add remote barrier model

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoFix makefile, set default nesting to 2
Mathieu Desnoyers [Thu, 26 Feb 2009 23:13:46 +0000 (18:13 -0500)] 
Fix makefile, set default nesting to 2

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoDefault nesting level to 1 (< 2)
Mathieu Desnoyers [Thu, 26 Feb 2009 23:03:24 +0000 (18:03 -0500)] 
Default nesting level to 1 (< 2)

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd reader nesting test
Mathieu Desnoyers [Thu, 26 Feb 2009 23:01:12 +0000 (18:01 -0500)] 
Add reader nesting test

Add readers with configurable nesting level.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd independent reader and writer progress checks
Mathieu Desnoyers [Wed, 25 Feb 2009 01:58:55 +0000 (20:58 -0500)] 
Add independent reader and writer progress checks

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agodual writer fix
Mathieu Desnoyers [Mon, 23 Feb 2009 07:02:54 +0000 (02:02 -0500)] 
dual writer fix

Make mutex between writers really atomic. Fixes the two flips run.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoRun 2 writers and show single flip error case
Mathieu Desnoyers [Mon, 23 Feb 2009 06:31:11 +0000 (01:31 -0500)] 
Run 2 writers and show single flip error case

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd ooomem and urcu checks
Mathieu Desnoyers [Mon, 23 Feb 2009 05:53:37 +0000 (00:53 -0500)] 
Add ooomem and urcu checks

Create a more simple model for ooo memory accesses and basic urcu checks.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoRestructure urcu_updater() to more accurately reflect actual failure scenario
Paul E. McKenney [Fri, 20 Feb 2009 16:56:20 +0000 (11:56 -0500)] 
Restructure urcu_updater() to more accurately reflect actual failure scenario

Restructure urcu_updater() to more accurately reflect actual failure
scenario.

This allows an easier transformation to force failure -- simple #ifdef
out the second counter flip out of urcu_updater()'s model of
"current synchronize_rcu()".

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoRemove spurious read-side infinite loops.
Paul E. McKenney [Fri, 20 Feb 2009 16:55:38 +0000 (11:55 -0500)] 
Remove spurious read-side infinite loops.

Remove spurious read-side infinite loops from urcu_reader() model.

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd _STORE_SHARED() and _LOAD_SHARED()
Mathieu Desnoyers [Fri, 13 Feb 2009 15:37:58 +0000 (10:37 -0500)] 
Add _STORE_SHARED() and _LOAD_SHARED()

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoTurn *_REMOTE into *_SHARED
Mathieu Desnoyers [Fri, 13 Feb 2009 12:25:33 +0000 (07:25 -0500)] 
Turn *_REMOTE into *_SHARED

"Paul E. McKenney" <paulmck@linux.vnet.ibm.com>:
I suspect that LOAD_SHARED() and STORE_SHARED() would be more intuitive.
But shouldn't we align with the Linux-kernel usage where reasonable?
(Yes, this can be a moving target, but there isn't much else that
currently supports this level of SMP function on quite the variety of
CPU architectures.)

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd missing cpu_relax in loop
Mathieu Desnoyers [Thu, 12 Feb 2009 21:53:23 +0000 (16:53 -0500)] 
Add missing cpu_relax in loop

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoFix compiler error.
Mathieu Desnoyers [Thu, 12 Feb 2009 21:45:19 +0000 (16:45 -0500)] 
Fix compiler error.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd smp_mc() to force_mb_single_thread so we don't assume anything from the OS.
Mathieu Desnoyers [Thu, 12 Feb 2009 21:35:01 +0000 (16:35 -0500)] 
Add smp_mc() to force_mb_single_thread so we don't assume anything from the OS.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd gitignore files
Mathieu Desnoyers [Thu, 12 Feb 2009 21:32:30 +0000 (16:32 -0500)] 
Add gitignore files

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoSupport architectures with non-coherent caches
Mathieu Desnoyers [Thu, 12 Feb 2009 21:29:55 +0000 (16:29 -0500)] 
Support architectures with non-coherent caches

Add
wmc(), rmc() and mc() which turns into barrier() or cache flush depending on the
architecture.

mb(), rmb() and wmb() turns into memory barriers or cache flush depending on the
architecture.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd support for x86 older than P4, with CONFIG_HAS_FENCE option
Mathieu Desnoyers [Thu, 12 Feb 2009 18:42:31 +0000 (13:42 -0500)] 
Add support for x86 older than P4, with CONFIG_HAS_FENCE option

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoFix warnings in urcutorture and use access once in urch.u
Paul E. McKenney [Thu, 12 Feb 2009 18:29:18 +0000 (13:29 -0500)] 
Fix warnings in urcutorture and use access once in urch.u

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoFix formal model nesting
Paul E. McKenney [Thu, 12 Feb 2009 18:25:05 +0000 (13:25 -0500)] 
Fix formal model nesting

Also, the original model I sent out has a minor bug that prevents it
from fully modeling the nested-read-side case.  The patch below fixes this.

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd read/write counts to test
Mathieu Desnoyers [Thu, 12 Feb 2009 06:44:34 +0000 (01:44 -0500)] 
Add read/write counts to test

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoFix force_mb_all_threads must be called within internal local
Mathieu Desnoyers [Thu, 12 Feb 2009 06:43:54 +0000 (01:43 -0500)] 
Fix force_mb_all_threads must be called within internal local

It iterates on threads, and must therefore be called within the mutex.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd barriers
Mathieu Desnoyers [Thu, 12 Feb 2009 06:00:00 +0000 (01:00 -0500)] 
Add barriers

Use smp_rmb() is busy-loops to make sure we re-read the variable.
Kick the reader threads we are waiting for after a few loops.
Documents memory ordering in rcu_read_lock().

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoRemove debug yield statements
Mathieu Desnoyers [Thu, 12 Feb 2009 04:52:31 +0000 (23:52 -0500)] 
Remove debug yield statements

Just too ugly.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agouse smp_*mb()
Mathieu Desnoyers [Thu, 12 Feb 2009 04:47:15 +0000 (23:47 -0500)] 
use smp_*mb()

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd Promela model
Mathieu Desnoyers [Thu, 12 Feb 2009 03:49:22 +0000 (22:49 -0500)] 
Add Promela model

From: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd missing memory barriers to ensure progress and remove an unnecessary ACCESS_ONCE
Mathieu Desnoyers [Wed, 11 Feb 2009 21:52:54 +0000 (16:52 -0500)] 
Add missing memory barriers to ensure progress and remove an unnecessary ACCESS_ONCE

[...]

So we could have the following reader+writer sequence :

Interleaved writer Sequence 2 and reader seq. 1.

Reader:
R.1 - read urcu_active_readers
S.2 - read counter
Writer:
B   - read other threads urcu_active_readers (there are none)
A.1 - flip counter
A.2 - read counter
Reader:
RS.2- write urcu_active_readers, depends on read counter and read
      urcu_active_readers
Here, the reader would have updated its counter as belonging to the old
q.s. period, but the writer will later wait for the new period. But
given the writer will eventually do a second flip+wait, the reader in
the other q.s. window will be caught by the second flip.

Therefore, we could be tempted to think that those mb() could be
unnecessary, which would lead to a scheme where urcu_active_readers and
urcu_gp_ctr are done in a completely random order one vs the other.
Let's see what it gives :

synchronize_rcu()

  force_mb_all_threads()  /*
                           * Orders pointer publication and
                           * (urcu_active_readers/urcu_gp_ctr accesses)
                           */
  switch_qparity()

    switch_next_urcu_qparity()  [just does counter flip 0->1]

    wait_for_quiescent_state()

      wait for all threads in parity 0

  switch_qparity()

    switch_next_urcu_qparity()  [Just does counter flip 1->0]

    wait_for_quiescent_state()

      Wait for all threads in parity 1

  force_mb_all_threads()  /*
                           * Orders
                           * (urcu_active_readers/urcu_gp_ctr accesses)
                           * and old data removal.
                           */

*but* ! There is a reason why we don't want to do this. If

    switch_next_urcu_qparity()  [Just does counter flip 1->0]

happens before the end of the previous

      Wait for all threads in parity 0

We enter in a situation where all newly coming readers will see the
parity bit as 0, although we are still waiting for that parity to end.
We end up in a state when the writer can be blocked forever (no possible
progress) if there are steadily readers subscribed for the data.

Basically, to put it differently, we could simply remove the bit
flipping from the writer and wait for *all* readers to exit their
critical section (even the ones simply interested in the new pointer).
But this shares the same problem the version above has, which is that we
end up in a situation where the writer won't progress if there are
always readers in a critical section.

The same applies to

    switch_next_urcu_qparity()  [Just does counter flip 0->1]

      wait for all threads in parity 0

If we don't put a mb() between those two (as I mistakenly did), we can
end up waiting for readers in parity 0 while the parity bit wasn't
flipped yet. oops. Same potential no-progress situation.

The ordering of memory reads in the reader for
urcu_active_readers/urcu_gp_ctr accesses does not seem to matter because
the data contains information about which q.s. period parity it is in.
In whichever order those variables are read seems to all work fine.

In the end, it's to insure that the writer will always progress that we
have to enforce smp_mb() between *all* switch_next_urcu_qparity and wait
for threads. Mine and yours.

The code in rcu_old_gp_ongoing (in my git tree) uses ACCESS_ONCE around
urcu_active_readers and urcu_gp_ctr reads. I think the ACCESS_ONCE
around urcu_gp_crt is useless because urcu_gp_ctr is only being modified
by ourself and we hold a mutex.

However, making sure that urcu_active_readers is only read once is
clearly required.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoEnhance test cases
Mathieu Desnoyers [Tue, 10 Feb 2009 18:57:53 +0000 (13:57 -0500)] 
Enhance test cases

New -n (to disable sleep in writer)
Now use a random delay for -w and -r.
Add -DDEBUG_FULL_MB option to use mb() in the reader rather than the
signal-based alternative.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoAdd comment in rcu_add_lock
Mathieu Desnoyers [Mon, 9 Feb 2009 19:05:19 +0000 (14:05 -0500)] 
Add comment in rcu_add_lock

Comment optimization to make it clear to the reader.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoFix int->long and keep a reader count of 1 in the global GP variable
Mathieu Desnoyers [Mon, 9 Feb 2009 18:52:41 +0000 (13:52 -0500)] 
Fix int->long and keep a reader count of 1 in the global GP variable

- Forgot a few migration from int to long
- Accelerate fast path by reading a GP variable which already has 1 reader
  count. This saves an increment in the fast path.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoFix RCU_GP_CTR_BIT
Mathieu Desnoyers [Mon, 9 Feb 2009 18:48:38 +0000 (13:48 -0500)] 
Fix RCU_GP_CTR_BIT

> > You lost me on this one:
> >
> >     sizeof(long) << 2 = 0x10
> >
> > I could believe the following (run on a 32-bit machine):
> >
> >     1 << (sizeof(long) * 8 - 1) = 0x80000000
> >
> > Or, if you were wanting to use a bit halfway up the word, perhaps this:
> >
> >     1 << (sizeof(long) * 4 - 1) = 0x8000
> >
> > Or am I confused?
>
> Well, I am at least partly confused.  You were wanting a low-order bit,
> so you want to lose the "- 1" above.  Here are some of the possibilities:
>
>       sizeof(long) = 0x4
>       sizeof(long) << 2 = 0x10
>       1 << (sizeof(long) * 8 - 1) = 0x80000000
>       1 << (sizeof(long) * 4) = 0x10000
>       1 << (sizeof(long) * 4 - 1) = 0x8000
>       1 << (sizeof(long) * 2) = 0x100
>       1 << (sizeof(long) * 2 - 1) = 0x80
>
> My guess is that 1 << (sizeof(long) * 4) and 1 << (sizeof(long) * 2)
> are of the most interest.
>

Exactly. I'll change it to :

I somehow thought this define was used as a bit number rather than the
bit mask.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
15 years agoFix data type, should now be long rather than int.
Mathieu Desnoyers [Mon, 9 Feb 2009 18:00:31 +0000 (13:00 -0500)] 
Fix data type, should now be long rather than int.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
This page took 0.043584 seconds and 4 git commands to generate.