Model Checked - MPSC queue + Rework State Machines

[mratsim]

Trying to fix:

• deadlock livelock happening in plain task parallelism and memory pool

  • Livelock in nqueens #122

• counting bugs:

  • [Mempool] Trying to allocate from a full arena #85
  • MPSC count can become negative #49

The implementation is run through CDS checker https://github.com/computersforpeace/model-checker but it internally uses dlmalloc mspace to replace uer's malloc and somehow it runs out of space and trigger this assert: https://github.com/computersforpeace/model-checker/blob/5c4efe5cd8bdfe1e85138396109876a121ca61d1/mymemory.cc#L166-L171

Might need to complete my own at #127 or use Relaxy (which cannot properly deal with compiler relaxed reordering unfortunately).

[mratsim]

This moRelaxed triggered the race detector every single time:

The rest of the changes were not checked

[mratsim]

sleep(xxx) seems like a bad test to test on-blocking sync as it leads to deadlock with Clang and/or on Mac:

• https://travis-ci.com/github/mratsim/weave/jobs/330952534#L902
• https://dev.azure.com/numforge/Weave/_build/results?buildId=529&view=logs&j=3e9b2beb-deba-59ca-c4e3-14471ee37ba8
• https://dev.azure.com/numforge/Weave/_build/results?buildId=529&view=logs&j=5336da5d-2772-5db2-cb26-68743e5bcd30

[mratsim]

Tried to use the RCMC VM (why GPL code with no source published?) at http://plv.mpi-sws.org/rcmc/

But:

• RCMC doesn't support malloc in threaded code, which makes it useless for testing queues (+ the source were removed ...)
• CDSChecker exhibits the same memory bug as on my machine
• Nidhugg doesn't implement C++11 memory model

So seems like even for C/C++ there is an lack of model checker to deal with C++11 concurrency bugs.

[mratsim]

Could there be a bug on OSX similar to https://linux-arm-kernel.infradead.narkive.com/jTmi6ANX/patch-arm-change-definition-of-cpu-relax-for-arm11mpcore

The cpu_relax() macro is often used in the body of busy-wait loops to ensure
that the variable being spun on is re-loaded for each iteration. On the
ARM11MPCore processor [where loads are prioritised over stores], spinning in
such a loop will prevent the write buffer from draining. If a write contained
in the write buffer indirectly affects the variable being spun on, there is a
potential for deadlock. This deadlock is experienced when executing the KGDB
testsuite on an SMP ARM11MPCore configuration.

This patch changes the definition of cpu_relax() to smp_mb() for ARMv6 cores,
forcing a flushing of the write buffer on SMP systems before the next load
takes place. If the Kernel is not compiled for SMP support, this will expand
to a barrier() as before.

Cc: Russell King - ARM Linux ***@arm.linux.org.uk
Acked-by: Catalin Marinas ***@arm.com
Signed-off-by: Will Deacon ***@arm.com

There is no obvious reason why this deadlock again, I don't use sleep:

weave/weave/parallel_tasks.nim

Lines 250 to 285 in c31e45f

	template dummy_cpt(): untyped =
	# Dummy computation
	# Calculate fib(30) iteratively
	var
	fib = 0
	f2 = 0
	f1 = 1
	for i in 2 .. 30:
	fib = f1 + f2
	f2 = f1
	f1 = fib
	proc sleepingLion(stop_ms: int64): int64 =
	let start = getTime()
	while true:
	let elapsed = inMilliseconds(getTime() - start)
	if elapsed >= stop_ms:
	return elapsed
	dummy_cpt()
	proc main2() =
	echo "Sanity check 3: isReady"
	const target = 123
	init(Weave)
	echo "Spawning sleeping thread for ", target, " ms"
	let start = getMonoTime()
	let f = spawn sleepingLion(123)
	while not f.isReady():
	cpuRelax()
	let stopReady = getMonoTime()
	let res = sync(f)
	let stopSync = getMonoTime()
	exit(Weave)

So it might be that with cpuRelax() the main thread leaves priority forever and deadlock ...

And ARM deadlocked too:

• https://travis-ci.com/github/mratsim/weave/jobs/331049281#L2634
• https://dev.azure.com/numforge/Weave/_build/results?buildId=542&view=logs&j=3e9b2beb-deba-59ca-c4e3-14471ee37ba8&t=1527aa7e-2e1a-5a51-e580-824ef3a68031
• https://dev.azure.com/numforge/Weave/_build/results?buildId=542&view=logs&j=5336da5d-2772-5db2-cb26-68743e5bcd30&t=c111748d-834b-55bf-d025-f190bfb75559

[mratsim]

Found the bug, there is a race condition in the test

   let f = spawn sleepingLion(123) 
   while not f.isReady(): 
     cpuRelax() 

The spinlock was (intentionally :/) not dispatching incoming steal requests. But if between initialization of the threadpool and spawn the freshly created threads didn't have time to send steal requests, the spawn stays in the root thread queue and the spinlock doesn't loadBalance so we get a deadlock.

[mratsim]

Still 2 bugs (maybe one):

• Stall on parallel_for_strided: https://travis-ci.com/github/mratsim/weave/jobs/331060040#L541-L545
• Still stall on the nestable GEMM, maybe related or maybe syncScope: https://travis-ci.com/github/mratsim/weave/jobs/331060041#L1262

Fixes for another time.