qemu

FORK: QEMU emulator
git clone https://git.neptards.moe/neptards/qemu.git
Log | Files | Refs | Submodules | LICENSE

aio_notify.promela (1888B)

      1 /*
      2  * This model describes the interaction between ctx->notify_me
      3  * and aio_notify().
      4  *
      5  * Author: Paolo Bonzini <pbonzini@redhat.com>
      6  *
      7  * This file is in the public domain.  If you really want a license,
      8  * the WTFPL will do.
      9  *
     10  * To simulate it:
     11  *     spin -p docs/aio_notify.promela
     12  *
     13  * To verify it:
     14  *     spin -a docs/aio_notify.promela
     15  *     gcc -O2 pan.c
     16  *     ./a.out -a
     17  *
     18  * To verify it (with a bug planted in the model):
     19  *     spin -a -DBUG docs/aio_notify.promela
     20  *     gcc -O2 pan.c
     21  *     ./a.out -a
     22  */
     23 
     24 #define MAX   4
     25 #define LAST  (1 << (MAX - 1))
     26 #define FINAL ((LAST << 1) - 1)
     27 
     28 bool notify_me;
     29 bool event;
     30 
     31 int req;
     32 int done;
     33 
     34 active proctype waiter()
     35 {
     36     int fetch;
     37 
     38     do
     39         :: true -> {
     40             notify_me++;
     41 
     42             if
     43 #ifndef BUG
     44                 :: (req > 0) -> skip;
     45 #endif
     46                 :: else ->
     47                     // Wait for a nudge from the other side
     48                     do
     49                         :: event == 1 -> { event = 0; break; }
     50                     od;
     51             fi;
     52 
     53             notify_me--;
     54 
     55             atomic { fetch = req; req = 0; }
     56             done = done | fetch;
     57         }
     58     od
     59 }
     60 
     61 active proctype notifier()
     62 {
     63     int next = 1;
     64 
     65     do
     66         :: next <= LAST -> {
     67             // generate a request
     68             req = req | next;
     69             next = next << 1;
     70 
     71             // aio_notify
     72             if
     73                 :: notify_me == 1 -> event = 1;
     74                 :: else           -> printf("Skipped event_notifier_set\n"); skip;
     75             fi;
     76 
     77             // Test both synchronous and asynchronous delivery
     78             if
     79                 :: 1 -> do
     80                             :: req == 0 -> break;
     81                         od;
     82                 :: 1 -> skip;
     83             fi;
     84         }
     85     od;
     86 }
     87 
     88 never { /* [] done < FINAL */
     89 accept_init:
     90         do
     91         :: done < FINAL -> skip;
     92         od;
     93 }