History log of /qemu/docs/spin/win32-qemu-event.promela (Results 1 – 2 of 2)
Revision Date Author Comments
# ac06724a 06-Jun-2017 Paolo Bonzini <pbonzini@redhat.com>

docs: create config/, devel/ and spin/ subdirectories

Developer documentation should be its own manual. As a start, move all
developer-oriented files to a separate directory.

Also move non-text fi

docs: create config/, devel/ and spin/ subdirectories

Developer documentation should be its own manual. As a start, move all
developer-oriented files to a separate directory.

Also move non-text files to their own directories: docs/config/ for
QEMU -readconfig input, and docs/spin/ for formal models to be used
with the SPIN model checker.

Reviewed-by: Daniel P. Berrange <berrange@redhat.com>
Signed-off-by: Paolo Bonzini <pbonzini@redhat.com>

show more ...


# 7c9b2bf6 12-Aug-2015 Paolo Bonzini <pbonzini@redhat.com>

qemu-thread: add a fast path to the Win32 QemuEvent

QemuEvents are used heavily by call_rcu. We do not want them to be slow,
but the current implementation does a kernel call on every invocation
of

qemu-thread: add a fast path to the Win32 QemuEvent

QemuEvents are used heavily by call_rcu. We do not want them to be slow,
but the current implementation does a kernel call on every invocation
of qemu_event_* and won't cut it.

So, wrap a Win32 manual-reset event with a fast userspace path. The
states and transitions are the same as for the futex and mutex/condvar
implementations, but the slow path is different of course. The idea
is to reset the Win32 event lazily, as part of a test-reset-test-wait
sequence. Such a sequence is, indeed, how QemuEvents are used by
RCU and other subsystems!

The patch includes a formal model of the algorithm.

Tested-by: Stefan Weil <sw@weilnetz.de>
Signed-off-by: Paolo Bonzini <pbonzini@redhat.com>
Signed-off-by: Stefan Weil <sw@weilnetz.de>

show more ...