1) Contents of the directory README this file mutex_zero_to_many.backup Specification file for test cases that do not use multiplicity based optimization many/print_time.c time printing function many/mutex.c Code generated by PROGRES for the unoptimized Mutex test cases many/ProtoMain.cc Runtime environment mutex_zero_to_one.backup Specification file for multiplicity optimized test cases one/print_time.c time printing function one/mutex.c Code generated by PROGRES for the multiplicity optimized Mutex test cases one/ProtoMain.cc Runtime environment 2) SW requirements - PROGRES (version 11.1) - rsh 3) Settings The LD_ASSUME_KERNEL environment variable should be set to 2.4.1 for newer kernels. 4) How to run a test case - uncomment the test case you want to run in lines 5739-5743 of many/mutex.c OR in lines 1956-1957 of one/mutex_mul.c - set runtime parameters in lines 5733-5734 of many/mutex.c OR in line 1951 of one/mutex_mul.c - recompile the code (by executing the make command) - run StartProto ------------------------------------------ many/mutex.c a) P_STS_sequence -> STS test set, multiplicity optimization OFF, parameter passing OFF, parallel execution OFF b) P_STS_sequence_PP -> STS test set, multiplicity optimization OFF, parameter passing ON, parallel execution OFF c) P_LTS_sequence -> LTS test set, multiplicity optimization OFF, parameter passing OFF, parallel execution OFF d) P_ALAP_sequence -> ALAP test set, multiplicity optimization OFF, parameter passing OFF, parallel execution OFF e) P_ALAP_sequence_par -> ALAP test set, multiplicity optimization OFF, parameter passing OFF, parallel execution ON ------------------------------------------ one/mutex_mul.c f) P_STS_sequence_mul -> STS test set, multiplicity optimization ON, parameter passing OFF, parallel execution OFF g) P_STS_sequence_mul_PP -> STS test set, multiplicity optimization ON, parameter passing ON, parallel execution OFF ------------------------------------------ 5) Additional information Please note that ProtoMain.cc files are not the same as the one in the default PROGRES 11.1 distribution. (The GUI has been switched off in the modified ProtoMain.cc file. All the modifications are commented and can be found by searching for the 'VG' string.) As PROGRES does not generate the necessary time printing commands, files many/mutex.c and one/mutex_mul.c were altered manually AFTER the code generation performed by PROGRES to include these commands (lines containing print_time()). Test case selection and setting parameters can be performed by modifying files many/mutex.c and one/mutex_mul.c as described above in Sec. 4).