Create a model of Mutex 1 (from the Mutex handout) in SPIN. Use that model to show that it is possible to have more than 1 process in the critical section at the same time. Strategically add printfs to your code so that the MSC contains meaningful information. Mail me (jones@cs.byu.edu) the msc.ps from a guided simulation that shows the error. Due last day of class.
Posted by jones at December 2, 2003 10:11 AM