lkml.org 
[lkml]   [2009]   [Feb]   [19]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
    Patch in this message
    /
    Date
    From
    Subject[[PATCH URCU formal]] Restructure urcu_updater() to more accurately reflect actual failure scenario.
    Restructure urcu_updater() to more accurately reflect actual failure
    scenario.

    This allows an easier transformation to force failure -- simple #ifdef
    out the second counter flip out of urcu_updater()'s model of
    "current synchronize_rcu()".

    Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
    ---
    formal-model/urcu.spin | 41 +++++++++++++++++++++++++++++++----------
    1 files changed, 31 insertions(+), 10 deletions(-)

    diff --git a/formal-model/urcu.spin b/formal-model/urcu.spin
    index eea18e8..3e18457 100644
    --- a/formal-model/urcu.spin
    +++ b/formal-model/urcu.spin
    @@ -187,10 +187,38 @@ proctype urcu_reader()

    proctype urcu_updater()
    {
    + /* prior synchronize_rcu(), second counter flip. */
    + need_mb = 1;
    + do
    + :: need_mb == 1 -> skip;
    + :: need_mb == 0 -> break;
    + od;
    + urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
    + need_mb = 1;
    + do
    + :: need_mb == 1 -> skip;
    + :: need_mb == 0 -> break;
    + od;
    + do
    + :: 1 ->
    + if
    + :: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
    + (urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
    + (urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK) ->
    + skip;
    + :: else -> break;
    + fi;
    + od;
    + need_mb = 1;
    + do
    + :: need_mb == 1 -> skip;
    + :: need_mb == 0 -> break;
    + od;
    +
    /* Removal statement, e.g., list_del_rcu(). */
    removed = 1;

    - /* synchronize_rcu(), first counter flip. */
    + /* current synchronize_rcu(), first counter flip. */
    need_mb = 1;
    do
    :: need_mb == 1 -> skip;
    @@ -204,15 +232,13 @@ proctype urcu_updater()
    od;
    do
    :: 1 ->
    - printf("urcu_gp_ctr=%x urcu_active_readers=%x\n", urcu_gp_ctr, urcu_active_readers);
    - printf("urcu_gp_ctr&0x7f=%x urcu_active_readers&0x7f=%x\n", urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK, urcu_active_readers & ~RCU_GP_CTR_NEST_MASK);
    if
    :: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
    (urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
    (urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK) ->
    skip;
    :: else -> break;
    - fi
    + fi;
    od;
    need_mb = 1;
    do
    @@ -220,10 +246,7 @@ proctype urcu_updater()
    :: need_mb == 0 -> break;
    od;

    - /* Erroneous removal statement, e.g., list_del_rcu(). */
    - /* removed = 1; */
    -
    - /* synchronize_rcu(), second counter flip. */
    + /* current synchronize_rcu(), second counter flip. */
    need_mb = 1;
    do
    :: need_mb == 1 -> skip;
    @@ -237,8 +260,6 @@ proctype urcu_updater()
    od;
    do
    :: 1 ->
    - printf("urcu_gp_ctr=%x urcu_active_readers=%x\n", urcu_gp_ctr, urcu_active_readers);
    - printf("urcu_gp_ctr&0x7f=%x urcu_active_readers&0x7f=%x\n", urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK, urcu_active_readers & ~RCU_GP_CTR_NEST_MASK);
    if
    :: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
    (urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
    --
    1.5.2.5


    \
     
     \ /
      Last update: 2009-02-20 03:01    [W:4.991 / U:0.096 seconds]
    ©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site