[qemu.git] / docs / aio_notify_bug.promela

/*
 * This model describes a bug in aio_notify.  If ctx->notifier is
 * cleared too late, a wakeup could be lost.
 *
 * 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 -DBUG docs/aio_notify_bug.promela
 *     gcc -O2 pan.c
 *     ./a.out -a -f
 *
 * 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 event;
bool req;
bool notifier_done;

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

active proctype notifier()
{
    do
        :: true -> {
            req = 1;
            if
               :: !USE_NOTIFY_ME || notify_me -> event = 1;
               :: else -> skip;
            fi
        }
        :: true -> break;
    od;
    notifier_done = 1;
}

#ifdef BUG
#define AIO_POLL                                                    \
    notify_me++;                                                    \
    if                                                              \
        :: !req -> {                                                \
            if                                                      \
                :: event -> skip;                                   \
            fi;                                                     \
        }                                                           \
        :: else -> skip;                                            \
    fi;                                                             \
    notify_me--;                                                    \
                                                                    \
    req = 0;                                                        \
    event = 0;
#else
#define AIO_POLL                                                    \
    notify_me++;                                                    \
    if                                                              \
        :: !req -> {                                                \
            if                                                      \
                :: event -> skip;                                   \
            fi;                                                     \
        }                                                           \
        :: else -> skip;                                            \
    fi;                                                             \
    notify_me--;                                                    \
                                                                    \
    event = 0;                                                      \
    req = 0;
#endif

active proctype waiter()
{
    do
       :: true -> AIO_POLL;
    od;
}

/* Same as waiter(), but disappears after a while.  */
active proctype temporary_waiter()
{
    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
21a03d17 PB	1	/*
	2	* This model describes a bug in aio_notify. If ctx->notifier is
	3	* cleared too late, a wakeup could be lost.
	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 -DBUG docs/aio_notify_bug.promela
	12	* gcc -O2 pan.c
	13	* ./a.out -a -f
	14	*
	15	* To verify the fixed version:
	16	* spin -a docs/aio_notify_bug.promela
	17	* gcc -O2 pan.c
	18	* ./a.out -a -f
	19	*
	20	* Add -DCHECK_REQ to test an alternative invariant and the
	21	* "notify_me" optimization.
	22	*/
	23
	24	int notify_me;
	25	bool event;
	26	bool req;
	27	bool notifier_done;
	28
	29	#ifdef CHECK_REQ
	30	#define USE_NOTIFY_ME 1
	31	#else
	32	#define USE_NOTIFY_ME 0
	33	#endif
	34
	35	active proctype notifier()
	36	{
	37	do
	38	:: true -> {
	39	req = 1;
	40	if
	41	:: !USE_NOTIFY_ME \|\| notify_me -> event = 1;
	42	:: else -> skip;
	43	fi
	44	}
	45	:: true -> break;
	46	od;
	47	notifier_done = 1;
	48	}
	49
	50	#ifdef BUG
	51	#define AIO_POLL \
	52	notify_me++; \
	53	if \
	54	:: !req -> { \
	55	if \
	56	:: event -> skip; \
	57	fi; \
	58	} \
	59	:: else -> skip; \
	60	fi; \
	61	notify_me--; \
	62	\
	63	req = 0; \
	64	event = 0;
65	#else
66	#define AIO_POLL \
67	notify_me++; \
68	if \
69	:: !req -> { \
70	if \
71	:: event -> skip; \
72	fi; \
73	} \
74	:: else -> skip; \
75	fi; \
76	notify_me--; \
77	\
78	event = 0; \
79	req = 0;
80	#endif
81
82	active proctype waiter()
83	{
84	do
85	:: true -> AIO_POLL;
86	od;
87	}
88
89	/* Same as waiter(), but disappears after a while. */
90	active proctype temporary_waiter()
91	{
92	do
93	:: true -> AIO_POLL;
94	:: true -> break;
95	od;
96	}
97
98	#ifdef CHECK_REQ
99	never {
100	do
101	:: req -> goto accept_if_req_not_eventually_false;
102	:: true -> skip;
103	od;
104
105	accept_if_req_not_eventually_false:
106	if
107	:: req -> goto accept_if_req_not_eventually_false;
108	fi;
109	assert(0);
110	}
111
112	#else
113	/* There must be infinitely many transitions of event as long
114	* as the notifier does not exit.
115	*
116	* If event stayed always true, the waiters would be busy looping.
117	* If event stayed always false, the waiters would be sleeping
118	* forever.
119	*/
120	never {
121	do
122	:: !event -> goto accept_if_event_not_eventually_true;
123	:: event -> goto accept_if_event_not_eventually_false;
124	:: true -> skip;
125	od;
126
127	accept_if_event_not_eventually_true:
128	if
129	:: !event && notifier_done -> do :: true -> skip; od;
130	:: !event && !notifier_done -> goto accept_if_event_not_eventually_true;
131	fi;
132	assert(0);
133
134	accept_if_event_not_eventually_false:
135	if
136	:: event -> goto accept_if_event_not_eventually_false;
137	fi;
138	assert(0);
139	}
140	#endif