[qemu.git] / docs / aio_notify_accept.promela

/*
 * This model describes the interaction between ctx->notified
 * and ctx->notifier.
 *
 * Author: Paolo Bonzini <[email protected]>
 *
 * This file is in the public domain.  If you really want a license,
 * the WTFPL will do.
 *
 * To verify the buggy version:
 *     spin -a -DBUG1 docs/aio_notify_bug.promela
 *     gcc -O2 pan.c
 *     ./a.out -a -f
 * (or -DBUG2)
 *
 * To verify the fixed version:
 *     spin -a docs/aio_notify_bug.promela
 *     gcc -O2 pan.c
 *     ./a.out -a -f
 *
 * Add -DCHECK_REQ to test an alternative invariant and the
 * "notify_me" optimization.
 */

int notify_me;
bool notified;
bool event;
bool req;
bool notifier_done;

#ifdef CHECK_REQ
#define USE_NOTIFY_ME 1
#else
#define USE_NOTIFY_ME 0
#endif

#ifdef BUG
#error Please define BUG1 or BUG2 instead.
#endif

active proctype notifier()
{
    do
        :: true -> {
            req = 1;
            if
               :: !USE_NOTIFY_ME || notify_me ->
#if defined BUG1
                   /* CHECK_REQ does not detect this bug! */
                   notified = 1;
                   event = 1;
#elif defined BUG2
                   if
                      :: !notified -> event = 1;
                      :: else -> skip;
                   fi;
                   notified = 1;
#else
                   event = 1;
                   notified = 1;
#endif
               :: else -> skip;
            fi
        }
        :: true -> break;
    od;
    notifier_done = 1;
}

#define AIO_POLL                                                    \
    notify_me++;                                                    \
    if                                                              \
        :: !req -> {                                                \
            if                                                      \
                :: event -> skip;                                   \
            fi;                                                     \
        }                                                           \
        :: else -> skip;                                            \
    fi;                                                             \
    notify_me--;                                                    \
                                                                    \
    atomic { old = notified; notified = 0; }                        \
    if                                                              \
       :: old -> event = 0;                                         \
       :: else -> skip;                                             \
    fi;                                                             \
                                                                    \
    req = 0;

active proctype waiter()
{
    bool old;

    do
       :: true -> AIO_POLL;
    od;
}

/* Same as waiter(), but disappears after a while.  */
active proctype temporary_waiter()
{
    bool old;

    do
       :: true -> AIO_POLL;
       :: true -> break;
    od;
}

#ifdef CHECK_REQ
never {
    do
        :: req -> goto accept_if_req_not_eventually_false;
        :: true -> skip;
    od;

accept_if_req_not_eventually_false:
    if
        :: req -> goto accept_if_req_not_eventually_false;
    fi;
    assert(0);
}

#else
/* There must be infinitely many transitions of event as long
 * as the notifier does not exit.
 *
 * If event stayed always true, the waiters would be busy looping.
 * If event stayed always false, the waiters would be sleeping
 * forever.
 */
never {
    do
        :: !event    -> goto accept_if_event_not_eventually_true;
        :: event     -> goto accept_if_event_not_eventually_false;
        :: true      -> skip;
    od;

accept_if_event_not_eventually_true:
    if
        :: !event && notifier_done  -> do :: true -> skip; od;
        :: !event && !notifier_done -> goto accept_if_event_not_eventually_true;
    fi;
    assert(0);

accept_if_event_not_eventually_false:
    if
        :: event     -> goto accept_if_event_not_eventually_false;
    fi;
    assert(0);
}
#endif
Commit	Line	Data
05e514b1 PB	1	/*
	2	* This model describes the interaction between ctx->notified
	3	* and ctx->notifier.
	4	*
	5	* Author: Paolo Bonzini <[email protected]>
	6	*
	7	* This file is in the public domain. If you really want a license,
	8	* the WTFPL will do.
	9	*
	10	* To verify the buggy version:
	11	* spin -a -DBUG1 docs/aio_notify_bug.promela
	12	* gcc -O2 pan.c
	13	* ./a.out -a -f
	14	* (or -DBUG2)
	15	*
	16	* To verify the fixed version:
	17	* spin -a docs/aio_notify_bug.promela
	18	* gcc -O2 pan.c
	19	* ./a.out -a -f
	20	*
	21	* Add -DCHECK_REQ to test an alternative invariant and the
	22	* "notify_me" optimization.
	23	*/
	24
	25	int notify_me;
	26	bool notified;
	27	bool event;
	28	bool req;
	29	bool notifier_done;
	30
	31	#ifdef CHECK_REQ
	32	#define USE_NOTIFY_ME 1
	33	#else
	34	#define USE_NOTIFY_ME 0
	35	#endif
	36
	37	#ifdef BUG
	38	#error Please define BUG1 or BUG2 instead.
	39	#endif
	40
	41	active proctype notifier()
	42	{
	43	do
	44	:: true -> {
	45	req = 1;
	46	if
	47	:: !USE_NOTIFY_ME \|\| notify_me ->
	48	#if defined BUG1
	49	/* CHECK_REQ does not detect this bug! */
	50	notified = 1;
	51	event = 1;
	52	#elif defined BUG2
	53	if
	54	:: !notified -> event = 1;
	55	:: else -> skip;
	56	fi;
	57	notified = 1;
	58	#else
	59	event = 1;
	60	notified = 1;
	61	#endif
	62	:: else -> skip;
	63	fi
	64	}
65	:: true -> break;
66	od;
67	notifier_done = 1;
68	}
69
70	#define AIO_POLL \
71	notify_me++; \
72	if \
73	:: !req -> { \
74	if \
75	:: event -> skip; \
76	fi; \
77	} \
78	:: else -> skip; \
79	fi; \
80	notify_me--; \
81	\
82	atomic { old = notified; notified = 0; } \
83	if \
84	:: old -> event = 0; \
85	:: else -> skip; \
86	fi; \
87	\
88	req = 0;
89
90	active proctype waiter()
91	{
92	bool old;
93
94	do
95	:: true -> AIO_POLL;
96	od;
97	}
98
99	/* Same as waiter(), but disappears after a while. */
100	active proctype temporary_waiter()
101	{
102	bool old;
103
104	do
105	:: true -> AIO_POLL;
106	:: true -> break;
107	od;
108	}
109
110	#ifdef CHECK_REQ
111	never {
112	do
113	:: req -> goto accept_if_req_not_eventually_false;
114	:: true -> skip;
115	od;
116
117	accept_if_req_not_eventually_false:
118	if
119	:: req -> goto accept_if_req_not_eventually_false;
120	fi;
121	assert(0);
122	}
123
124	#else
125	/* There must be infinitely many transitions of event as long
126	* as the notifier does not exit.
127	*
128	* If event stayed always true, the waiters would be busy looping.
129	* If event stayed always false, the waiters would be sleeping
130	* forever.
131	*/
132	never {
133	do
134	:: !event -> goto accept_if_event_not_eventually_true;
135	:: event -> goto accept_if_event_not_eventually_false;
136	:: true -> skip;
137	od;
138
139	accept_if_event_not_eventually_true:
140	if
141	:: !event && notifier_done -> do :: true -> skip; od;
142	:: !event && !notifier_done -> goto accept_if_event_not_eventually_true;
143	fi;
144	assert(0);
145
146	accept_if_event_not_eventually_false:
147	if
148	:: event -> goto accept_if_event_not_eventually_false;
149	fi;
150	assert(0);
151	}
152	#endif