urcu.git
10 years agoMerge branch 'master' of lttng.org:/home/git/userspace-rcu
Mathieu Desnoyers [Wed, 17 Jun 2009 16:31:58 +0000 (12:31 -0400)] 
Merge branch 'master' of lttng.org:/home/git/userspace-rcu

10 years agoFix typo in license file
Mathieu Desnoyers [Wed, 17 Jun 2009 16:31:36 +0000 (12:31 -0400)] 
Fix typo in license file

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd cpu time
compudj [Tue, 16 Jun 2009 21:40:28 +0000 (17:40 -0400)] 
Add cpu time

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd output to runall.log
compudj [Tue, 16 Jun 2009 21:29:25 +0000 (17:29 -0400)] 
Add output to runall.log

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoFix test_looplen, use double-precition arithmetic
Paul E. McKenney [Sat, 13 Jun 2009 23:53:05 +0000 (19:53 -0400)] 
Fix test_looplen, use double-precition arithmetic

Here you go!!!

        [root@perfsqh userspace-rcu]# ./test_looplen
        CALIBRATION : 0 cycles per loop

Hmmm...  Probably not what you had in mind.  Breaking out the
floating-point arithmetic:

        [root@perfsqh userspace-rcu]# ./test_looplen
        CALIBRATION : 0.386172 cycles per loop
        time_tot = 4049312, LOOPS = 1048576, TESTS = 10

More helpful?  ;-)

                                                Thanx, Paul

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoOther timing tests, update cache line size
Mathieu Desnoyers [Sat, 13 Jun 2009 23:18:38 +0000 (19:18 -0400)] 
Other timing tests, update cache line size

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoDeal with POWER5+ 256B L3 cachefalse sharing for per thread lock
Mathieu Desnoyers [Sat, 13 Jun 2009 23:10:31 +0000 (19:10 -0400)] 
Deal with POWER5+ 256B L3 cachefalse sharing for per thread lock

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd looplen cycle test
Mathieu Desnoyers [Sat, 13 Jun 2009 21:52:43 +0000 (17:52 -0400)] 
Add looplen cycle test

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoFix affinity in test script
Paul E. McKenney [Sat, 13 Jun 2009 21:02:36 +0000 (17:02 -0400)] 
Fix affinity in test script

You need to change the script!!!  See patch below.  All prior results
with more than 32 CPUs are bogus because the -a arguments confined the
threads to only 32 CPUs (the even-numbered ones from zero to 62).

Allow 64 CPUs.  Really needs to do the calculation based on the
stride and the number of CPUs, but a quick hack for now.

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
10 years agoAdded a few points to the readercs test
Mathieu Desnoyers [Sat, 13 Jun 2009 19:00:03 +0000 (15:00 -0400)] 
Added a few points to the readercs test

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoUpdate update fraction test
Mathieu Desnoyers [Sat, 13 Jun 2009 18:51:02 +0000 (14:51 -0400)] 
Update update fraction test

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoUpdate readcslen test to use NUM_CPUS readers
Mathieu Desnoyers [Sat, 13 Jun 2009 18:40:53 +0000 (14:40 -0400)] 
Update readcslen test to use NUM_CPUS readers

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoFix perthreadlock test
Mathieu Desnoyers [Sat, 13 Jun 2009 05:19:33 +0000 (01:19 -0400)] 
Fix perthreadlock test

segmentation fault when 0 readers due to incorrect mutex array indexing (int vs
long types).

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAllow use on high-end Power systems.
Paul E. McKenney [Sat, 13 Jun 2009 04:59:14 +0000 (00:59 -0400)] 
Allow use on high-end Power systems.

Power systems self-identify as ppc64 rather than powerpc.  Add the
corresponding logic to the Makefile.

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoUpdate fraction update
Mathieu Desnoyers [Fri, 12 Jun 2009 22:44:32 +0000 (18:44 -0400)] 
Update fraction update

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoUpdate update-fraction test
Mathieu Desnoyers [Fri, 12 Jun 2009 22:42:05 +0000 (18:42 -0400)] 
Update update-fraction test

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoUpdate test
Mathieu Desnoyers [Fri, 12 Jun 2009 19:28:29 +0000 (15:28 -0400)] 
Update test

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd runall.sh test
Mathieu Desnoyers [Fri, 12 Jun 2009 19:16:29 +0000 (15:16 -0400)] 
Add runall.sh test

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoFix alignment of test names
Mathieu Desnoyers [Fri, 12 Jun 2009 18:30:19 +0000 (14:30 -0400)] 
Fix alignment of test names

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAlign the summary result
Mathieu Desnoyers [Fri, 12 Jun 2009 18:28:18 +0000 (14:28 -0400)] 
Align the summary result

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd verbose mode
Mathieu Desnoyers [Fri, 12 Jun 2009 18:18:46 +0000 (14:18 -0400)] 
Add verbose mode

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoPrint reader duration
Mathieu Desnoyers [Fri, 12 Jun 2009 17:52:29 +0000 (13:52 -0400)] 
Print reader duration

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoDelay reader in loops, not us
Mathieu Desnoyers [Fri, 12 Jun 2009 17:51:20 +0000 (13:51 -0400)] 
Delay reader in loops, not us

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd -c option for read-side C.S. length to tests
Mathieu Desnoyers [Fri, 12 Jun 2009 17:31:02 +0000 (13:31 -0400)] 
Add -c option for read-side C.S. length to tests

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agofix runtests.sh
Mathieu Desnoyers [Wed, 10 Jun 2009 22:44:58 +0000 (18:44 -0400)] 
fix runtests.sh

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoruntests include mutex test
Mathieu Desnoyers [Wed, 10 Jun 2009 22:43:37 +0000 (18:43 -0400)] 
runtests include mutex test

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd test mutex
Mathieu Desnoyers [Wed, 10 Jun 2009 22:43:07 +0000 (18:43 -0400)] 
Add test mutex

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd set affinity -a option to tests
Mathieu Desnoyers [Wed, 10 Jun 2009 22:40:26 +0000 (18:40 -0400)] 
Add set affinity -a option to tests

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoUnlikely for tests
Mathieu Desnoyers [Wed, 10 Jun 2009 18:59:13 +0000 (14:59 -0400)] 
Unlikely for tests

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd i586 i686 to Makefile
Mathieu Desnoyers [Wed, 10 Jun 2009 18:47:02 +0000 (14:47 -0400)] 
Add i586 i686 to Makefile

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoUpdate readme
Mathieu Desnoyers [Wed, 10 Jun 2009 17:38:42 +0000 (13:38 -0400)] 
Update readme

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd Makefile and Makefile64 architecture autodetection
Mathieu Desnoyers [Wed, 10 Jun 2009 17:35:30 +0000 (13:35 -0400)] 
Add Makefile and Makefile64 architecture autodetection

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoMake sure the rwlock and per thread lock could detect races
Mathieu Desnoyers [Wed, 10 Jun 2009 16:06:42 +0000 (12:06 -0400)] 
Make sure the rwlock and per thread lock could detect races

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoFix deadlock in qsbr code
Mathieu Desnoyers [Wed, 10 Jun 2009 16:01:47 +0000 (12:01 -0400)] 
Fix deadlock in qsbr code

Readers must go offline because they unregister.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoFix qsbr urcu implementation
Mathieu Desnoyers [Wed, 10 Jun 2009 15:55:06 +0000 (11:55 -0400)] 
Fix qsbr urcu implementation

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoUpdate makefiles
Mathieu Desnoyers [Wed, 10 Jun 2009 15:53:59 +0000 (11:53 -0400)] 
Update makefiles

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd missing void to function declaration
Mathieu Desnoyers [Wed, 10 Jun 2009 15:51:03 +0000 (11:51 -0400)] 
Add missing void to function declaration

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoUse more lightweight timer mechanism in test
Mathieu Desnoyers [Wed, 10 Jun 2009 15:31:46 +0000 (11:31 -0400)] 
Use more lightweight timer mechanism in test

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoRemove unneeded signal-based MB from QSBR rcu
Mathieu Desnoyers [Wed, 10 Jun 2009 14:17:35 +0000 (10:17 -0400)] 
Remove unneeded signal-based MB from QSBR rcu

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoFix signal handler installation
Pierre-Marc Fournier [Tue, 9 Jun 2009 21:54:49 +0000 (17:54 -0400)] 
Fix signal handler installation

The signal handler is not being set in conformance with the sigaction
manpage. Because of this, it is probably not set at all. Valgrind also
generates an error. This patch fixes this.

Signed-off-by: Pierre-Marc Fournier <pierre-marc.fournier@polymtl.ca>
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd missing urcu-qsbr
Mathieu Desnoyers [Tue, 9 Jun 2009 21:50:23 +0000 (17:50 -0400)] 
Add missing urcu-qsbr

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd runtests.sh
Mathieu Desnoyers [Tue, 9 Jun 2009 18:20:08 +0000 (14:20 -0400)] 
Add runtests.sh

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd mb urcu flavor test
Mathieu Desnoyers [Tue, 9 Jun 2009 18:15:56 +0000 (14:15 -0400)] 
Add mb urcu flavor test

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd perthread lock scaling test
Mathieu Desnoyers [Tue, 9 Jun 2009 18:09:21 +0000 (14:09 -0400)] 
Add perthread lock scaling test

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoMove test start time closer to enable
Mathieu Desnoyers [Tue, 9 Jun 2009 17:55:00 +0000 (13:55 -0400)] 
Move test start time closer to enable

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd rwlock scalability test
Mathieu Desnoyers [Tue, 9 Jun 2009 16:50:37 +0000 (12:50 -0400)] 
Add rwlock scalability test

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd scalability qsbr test
Mathieu Desnoyers [Tue, 9 Jun 2009 16:41:21 +0000 (12:41 -0400)] 
Add scalability qsbr test

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoModify test_urcu to make more suitable for scalability benchmark
Mathieu Desnoyers [Tue, 9 Jun 2009 16:29:02 +0000 (12:29 -0400)] 
Modify test_urcu to make more suitable for scalability benchmark

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd number of reader/writers parameters to tests
Mathieu Desnoyers [Mon, 8 Jun 2009 18:57:27 +0000 (14:57 -0400)] 
Add number of reader/writers parameters to tests

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd QSBR RCU timing tests
Mathieu Desnoyers [Mon, 8 Jun 2009 18:41:37 +0000 (14:41 -0400)] 
Add QSBR RCU timing tests

urcu-qsbr can be used for QSBR-based RCU.

Currently not built as a full-blown library .so, but could.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoupdate test timings for writer
Mathieu Desnoyers [Mon, 8 Jun 2009 18:12:50 +0000 (14:12 -0400)] 
update test timings for writer

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd per thread lock test case
Mathieu Desnoyers [Mon, 8 Jun 2009 17:37:39 +0000 (13:37 -0400)] 
Add per thread lock test case

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAnother ooo mem isched update
Mathieu Desnoyers [Thu, 4 Jun 2009 19:45:40 +0000 (15:45 -0400)] 
Another ooo mem isched update

really just to simplify the LTL formula.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoUpdate isched ooomem model
Mathieu Desnoyers [Thu, 4 Jun 2009 19:43:42 +0000 (15:43 -0400)] 
Update isched ooomem model

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoUpdate ooo isched test
Mathieu Desnoyers [Thu, 4 Jun 2009 19:40:12 +0000 (15:40 -0400)] 
Update ooo isched test

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoUse nicer LTL formula with eventually for ooomem model
Mathieu Desnoyers [Thu, 4 Jun 2009 18:58:21 +0000 (14:58 -0400)] 
Use nicer LTL formula with eventually for ooomem model

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd speculative execution (prefetch) to model
Mathieu Desnoyers [Thu, 4 Jun 2009 13:26:57 +0000 (09:26 -0400)] 
Add speculative execution (prefetch) to model

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoFix comment on top of oomem two writes model
Mathieu Desnoyers [Wed, 3 Jun 2009 20:41:49 +0000 (16:41 -0400)] 
Fix comment on top of oomem two writes model

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd Intel ipi urcu model run results
Mathieu Desnoyers [Wed, 3 Jun 2009 14:15:45 +0000 (10:15 -0400)] 
Add Intel ipi urcu model run results

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoAdd multiple arch support (alpha, intel, powerpc)
Mathieu Desnoyers [Wed, 3 Jun 2009 04:48:08 +0000 (00:48 -0400)] 
Add multiple arch support (alpha, intel, powerpc)

A simple define controls the architecture tested.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 years agoVerification run #1, ipi and no-ipi results
Mathieu Desnoyers [Sat, 30 May 2009 22:31:09 +0000 (18:31 -0400)] 
Verification run #1, ipi and no-ipi results

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
10 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>
This page took 0.058847 seconds and 4 git commands to generate.