Fix formal model nesting
authorPaul E. McKenney <paulmck@linux.vnet.ibm.com>
Thu, 12 Feb 2009 18:25:05 +0000 (13:25 -0500)
committerMathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
Thu, 12 Feb 2009 18:25:05 +0000 (13:25 -0500)
commitf321bf383dd9b5940b31e4db6c9e18a5abaa0213
treec48e4cacf98dbcaf034f2ae93db813d411579b6c
parent1eec319e7724ac54bb3174f367ca9391840fcdc1
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>
formal-model/urcu.spin
This page took 0.025967 seconds and 4 git commands to generate.