Join GitHub today
GitHub is home to over 31 million developers working together to host and review code, manage projects, and build software together.Sign up
Thread lock up #6771
Original bug ID: 6771
Especially on windows (but also on Linux) it seems that:
Steps to reproduce
Test case in attachment. It is a stripped down Coq, sorry for the not exactly clean and readable code.
"server" spawns "client mitm" that in turn spawns "client".
The MITM runs two threads talking with server and client respectively.
On Linux things mostly work here, and rarely hang (and only if I add to the picture more threads). On my Windows 7 virtual machine the test case hangs systematically.
This bug affects Coq 8.5beta1 (where a huge hack works around it).
Comment author: enrico
Could be, on Windows we use sockets (the code I've attached can do with pipes too but on Windows we go for sockets). From the bug report you link it is
But I'm sure I've seen it hang on Linux too, even if today I cannot reproduce
Comment author: @damiendoligez
I'm pretty sure this is a duplicate of #5325: you have one thread blocked on read on a socket, and another thread tries to write, and blocks.
In your case, there is an easy workaround: use two sockets instead of one (see attached diff, which fixes the problem on your test case).
This bug won't be fixed before 4.02.2.