cachepc-qemu

Fork of AMDESE/qemu with changes for cachepc side-channel attack
git clone https://git.sinitax.com/sinitax/cachepc-qemu
Log | Files | Refs | Submodules | LICENSE | sfeed.txt

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
     28bool notify_me;
     29bool event;
     30
     31int req;
     32int done;
     33
     34active 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
     61active 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
     88never { /* [] done < FINAL */
     89accept_init:
     90        do
     91        :: done < FINAL -> skip;
     92        od;
     93}