blob: c446a71555339f0f79ca758b7f08cb1267ac05cd [file] [log] [blame]
/*
* This model describes the implementation of QemuEvent in
* util/qemu-thread-win32.c.
*
* Author: Paolo Bonzini <pbonzini@redhat.com>
*
* This file is in the public domain. If you really want a license,
* the WTFPL will do.
*
* To verify it:
* spin -a docs/event.promela
* gcc -O2 pan.c -DSAFETY
* ./a.out
*/
bool event;
int value;
/* Primitives for a Win32 event */
#define RAW_RESET event = false
#define RAW_SET event = true
#define RAW_WAIT do :: event -> break; od
#if 0
/* Basic sanity checking: test the Win32 event primitives */
#define RESET RAW_RESET
#define SET RAW_SET
#define WAIT RAW_WAIT
#else
/* Full model: layer a userspace-only fast path on top of the RAW_*
* primitives. SET/RESET/WAIT have exactly the same semantics as
* RAW_SET/RAW_RESET/RAW_WAIT, but try to avoid invoking them.
*/
#define EV_SET 0
#define EV_FREE 1
#define EV_BUSY -1
int state = EV_FREE;
int xchg_result;
#define SET if :: state != EV_SET -> \
atomic { /* xchg_result=xchg(state, EV_SET) */ \
xchg_result = state; \
state = EV_SET; \
} \
if :: xchg_result == EV_BUSY -> RAW_SET; \
:: else -> skip; \
fi; \
:: else -> skip; \
fi
#define RESET if :: state == EV_SET -> atomic { state = state | EV_FREE; } \
:: else -> skip; \
fi
int tmp1, tmp2;
#define WAIT tmp1 = state; \
if :: tmp1 != EV_SET -> \
if :: tmp1 == EV_FREE -> \
RAW_RESET; \
atomic { /* tmp2=cas(state, EV_FREE, EV_BUSY) */ \
tmp2 = state; \
if :: tmp2 == EV_FREE -> state = EV_BUSY; \
:: else -> skip; \
fi; \
} \
if :: tmp2 == EV_SET -> tmp1 = EV_SET; \
:: else -> tmp1 = EV_BUSY; \
fi; \
:: else -> skip; \
fi; \
assert(tmp1 != EV_FREE); \
if :: tmp1 == EV_BUSY -> RAW_WAIT; \
:: else -> skip; \
fi; \
:: else -> skip; \
fi
#endif
active proctype waiter()
{
if
:: !value ->
RESET;
if
:: !value -> WAIT;
:: else -> skip;
fi;
:: else -> skip;
fi;
assert(value);
}
active proctype notifier()
{
value = true;
SET;
}