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>
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>
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>
Mathieu Desnoyers [Wed, 10 Jun 2009 15:53:59 +0000 (11:53 -0400)]
Update makefiles
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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?
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
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>
This page took 0.043418 seconds and 4 git commands to generate.
projects / userspace-rcu.git / log
