urcu:formal-model

Last commit made on 2012-10-09
Get this branch:
git clone -b formal-model https://git.launchpad.net/urcu

Branch merges

Branch information

Name:
formal-model
Repository:
lp:urcu

Recent commits

2937ba8... by Mathieu Desnoyers on 2012-10-09

Revert "spinlock model: Simplify state-space"

This reverts commit a9227ee907160443d0e4b1639b274ab9278d92fa.

Need to study impact on progress.

Signed-off-by: Mathieu Desnoyers <email address hidden>

9b305d2... by Mathieu Desnoyers on 2012-10-09

Revert "Style Cleanup"

This reverts commit 03126291913d3c2df1d92137cf82767d9b490ade.

Need to study impact on progress.

Signed-off-by: Mathieu Desnoyers <email address hidden>

7ecea09... by Mathieu Desnoyers on 2012-10-09

Revert "ticketlock model: state-space simplication"

This reverts commit d149fa02aaafa08c2d02712afd3cbbbc5f8d5f67.

Need to study impact on progress.

Signed-off-by: Mathieu Desnoyers <email address hidden>

d149fa0... by Mathieu Desnoyers on 2012-10-08

ticketlock model: state-space simplication

Signed-off-by: Mathieu Desnoyers <email address hidden>

0312629... by Mathieu Desnoyers on 2012-10-08

Style Cleanup

Signed-off-by: Mathieu Desnoyers <email address hidden>

a9227ee... by Mathieu Desnoyers on 2012-10-08

spinlock model: Simplify state-space

Remove useless busy-looping, useless in Promela. Same semantic as the
new code:

Quoting Michel Dagenais <email address hidden>:

> http://spinroot.com/spin/Man/condition.html
> In Promela , a standalone expression is a valid statement. Execution
> of a condition statement is blocked until the expression evaluates to
> a non-zero value (or, equivalently, to the boolean value true ).
>
> http://spinroot.com/spin/Man/separators.html
> The semicolon and the arrow are equivalent statement separators in
> Promela. The convention is to reserve the use of the arrow separator
> to follow condition statements. The arrow symbol can thus be used to
> visually identify those points in the code where execution could
> block.

Signed-off-by: Mathieu Desnoyers <email address hidden>

2e33016... by Mathieu Desnoyers on 2011-08-29

Add back urcu QSBR selective wakeup model

Signed-off-by: Mathieu Desnoyers <email address hidden>

ef78165... by Mathieu Desnoyers on 2011-08-27

Add 1ton readonly waiter model

Signed-off-by: Mathieu Desnoyers <email address hidden>

3646de2... by Mathieu Desnoyers on 2011-08-27

1to1 selective wakeup: add misorder injection test

Signed-off-by: Mathieu Desnoyers <email address hidden>

fda9aff... by Mathieu Desnoyers on 2011-08-27

Update nto1 selective model

The nto1 selective wakeup model introduced by Paolo was:

a) too complex (tried to model the full-blown RCU rather than a simple
   queue system)
b) did not model progress with wakers running for a limited amount of
   iterations, only with wakers running infinitely often (which
   therefore does not prove anything).

What we really want to model here is what happens if we have wakers
running a few times, and then not running for a very long time: can we
end up with a missed wakeup, and therefore end up with an enqueued entry
but with the waiter waiting forever ?

Signed-off-by: Mathieu Desnoyers <email address hidden>