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 attemptin开发者_Go百科g 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.
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:
- If your mutex is recursive (ie can the same thread lock it multiple times) then ensure you do some reference counting tests.
- With your global variable that you modify it would be best if this was a varible that can't be written to atomically. For example if you are on an 8 bit platform then use a 16 or 32 bit variable that requires multiple assembly instructions to write.
- Carefully examine the assembly listing. Depending on the hardware platform though the assembly does not translate directly to how the code might be optimised...
- Get someone else, who didn't write the code, to also write some tests.
- test on as many different machines with different specs as you can (assuming that this is 'general purpose' and not for a specific hardware setup)
Good luck!
This reminds me of this question about FIFO semaphore test. In a nutshell my answer was:
- Even if you have a specification, maybe it doesn't convey your intention exactly
- You can prove that the algorithm fulfills the specification, but not the code (D. Knuth)
- Test reveal only the presence of bug, not their absence (Dijkstra)
So your proposition seem reasonably the best to do. If you want to increase your confidence, use fuzzing to randomize scheduling and input.
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.
精彩评论