aboutsummaryrefslogtreecommitdiff
path: root/docs/tcg-exclusive.promela
AgeCommit message (Collapse)AuthorFilesLines
2016-09-27cpus-common: lock-free fast path for cpu_exec_start/endPaolo Bonzini1-3/+50
Set cpu->running without taking the cpu_list lock, only requiring it if there is a concurrent exclusive section. This requires adding a new field to CPUState, which records whether a running CPU is being counted in pending_cpus. When an exclusive section is started concurrently with cpu_exec_start, cpu_exec_start can use the new field to determine if it has to wait for the end of the exclusive section. Likewise, cpu_exec_end can use it to see if start_exclusive is waiting for that CPU. This a separate patch for easier bisection of issues. Signed-off-by: Paolo Bonzini <pbonzini@redhat.com>
2016-09-27cpus-common: simplify locking for start_exclusive/end_exclusivePaolo Bonzini1-1/+3
It is not necessary to hold qemu_cpu_list_mutex throughout the exclusive section, because no other exclusive section can run while pending_cpus != 0. exclusive_idle() is called in cpu_exec_start(), and that prevents any CPUs created after start_exclusive() from entering cpu_exec() during an exclusive section. Reviewed-by: Richard Henderson <rth@twiddle.net> Reviewed-by: Alex Bennée <alex.bennee@linaro.org> Signed-off-by: Paolo Bonzini <pbonzini@redhat.com>
2016-09-27cpus-common: remove redundant call to exclusive_idle()Paolo Bonzini1-1/+0
No need to call exclusive_idle() from cpu_exec_end since it is done immediately afterwards in cpu_exec_start. Any exclusive section could run as soon as cpu_exec_end leaves, because cpu->running is false and the mutex is not taken, so the call does not add any protection either. Reviewed-by: Richard Henderson <rth@twiddle.net> Reviewed-by: Alex Bennée <alex.bennee@linaro.org> Signed-off-by: Paolo Bonzini <pbonzini@redhat.com>
2016-09-27docs: include formal model for TCG exclusive sectionsPaolo Bonzini1-0/+177
Reviewed-by: Richard Henderson <rth@twiddle.net> Signed-off-by: Paolo Bonzini <pbonzini@redhat.com>