Fix urcu controldataflow model remote barriers
authorMathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
Wed, 20 May 2009 04:25:17 +0000 (00:25 -0400)
committerMathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
Wed, 20 May 2009 04:25:17 +0000 (00:25 -0400)
commit19d8de31dc92430df89d90e8ba76212b764afd44
tree3eac8d589cb0f49059d5fea0f7b9e3bed0c92bc8
parenta60dadc52fed020644e44b346c438a3ccd3a5026
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>
formal-model/urcu-controldataflow/urcu.spin
This page took 0.024401 seconds and 4 git commands to generate.