What is the best way to test an implementation of a mutex is indeed correct? (It is necessary to implement a mutex, reuse is not a viable option)
The best I have come up with is to have many (N) concurrent threads iteratively attempting to access the protected region (I) times, which has a side effect (e.g. update to a global) so that the number of accesses + writes can be counted to ensure that the number of updates to the global is exactly (N)*(I).
Any other suggestions?
Formal proof is better than testing for this kind of thing.
Testing will show you that -- as long as you're not unlucky -- it all worked. But a test is a blunt instrument; it can fail to execute the exact right sequence to cause failure.
It's too hard to test every possible sequence of operations available in the hardware to be sure your mutex works under all circumstances.
Testing is not without value; it shows that you didn't make any obvious coding errors.
But you really need a more formal code inspection to demonstrate that it does the right things at the right times so that one client will atomically seize the lock resource required for proper mutex. In many platforms, there are special instructions to implement this, and if you're using one of those, you have a fighting chance of getting it right.
Similarly, you have to show that the release is atomic.
With something like a mutex, we get back to the old rule that testing can only demonstrate the presence of bugs, not the absence. A year of testing will probably tell you less than simply putting the code up for inspection, and asking if anybody sees a problem with it.
If the proof stuff doesn't work out for you, then go with the testing one. Be sure to test all the possible use cases. Find out how exactly this thing will be used, who will be using it and, again, how it will be used. When you go the testing route be sure to run each test for each scenario a ton of times (millions, billions, as many as you can possibly get in with the testing time you have).
Try to be random because randomness will give you the best chance to cover all scenarios in a limited number of tests. Be sure to use data that will be used and data that may not be used but could be used and make sure the data doesn't mess up the locks.
BTW, unless you know a ton about mathematics and formal methods you will have no chance of actually coming up with a proof.
This reminds me of this question about FIFO semaphore test. In a nutshell my answer was:
So your proposition seem reasonably the best to do. If you want to increase your confidence, use fuzzing to randomize scheduling and input.
I'm with everyone else that this is incredibly difficult to prove conclusively, I have no idea how to do it - not helpful I know!
When you say implement a mutex and that reuse is not an option, is that for technical reasons like there is no Mutex implementation on the platform/OS that you are using or some other reason? Is wrapping some form of OS level 'lock' and calling it your Mutex implementation an option, eg CriticalSection on windoze, posix Condition Variables? If you can wrap a lower level OS lock then your chance of getting it right are much higher.
In case you have not already done so go and read Herb Sutter's Effective Concurrency articles. There should be some stuff in these worth something to you.
Anyway, some things to consider in your tests:
Good luck!