[mc] Add a test to examplify that we should handle mutex operations in MC
In this test, we have two senders sending one message to a common
receiver. The receiver should be able to see any ordering between the
two messages. If we model-check the application with assertions on a
specific order of the messages (see the assertions in the receiver
code), it should fail because both ordering are possible.
If the senders sends the message directly, the current version of the
MC finds that the ordering may differ and the MC find a
counter-example.
However, if the senders send the message in a mutex, the MC always let
the first process take the mutex because it thinks that the effect of
a mutex is purely local: the ordering of the messages is always the
same and the MC does not find the counter-example.
