source:
CIVL/examples/concurrency/Makefile@
85b7e48
| Last change on this file since 85b7e48 was 7e8e35c, checked in by , 12 years ago | |
|---|---|
|
|
| File size: 1.4 KB | |
| Rev | Line | |
|---|---|---|
| [72c01cc] | 1 | CIVL=civl |
| 2 | VERIFY=$(CIVL) verify | |
| 3 | ||
| [9fb69d3] | 4 | all: adder adderBad bank barrier barrier2 \ |
| 5 | barrierBad blockAdder blockAdderBad dining \ | |
| 6 | diningBad locksBad locksBad10 locksGood \ | |
| 7 | spawn spawn2 spawnBad | |
| 8 | ||
| [72c01cc] | 9 | adder: adder.cvl |
| [7e8e35c] | 10 | $(VERIFY) -inputB=5 adder.cvl |
| [72c01cc] | 11 | |
| 12 | adderBad: adderBad.cvl | |
| [7e8e35c] | 13 | $(VERIFY) -inputB=4 -min adderBad.cvl |
| [72c01cc] | 14 | $(CIVL) replay adderBad.cvl |
| [30cc8b7] | 15 | |
| [72c01cc] | 16 | bank: bank.cvl |
| [7e8e35c] | 17 | $(VERIFY) -inputNUM_ACCOUNTS=3 bank.cvl |
| [30cc8b7] | 18 | |
| [72c01cc] | 19 | barrier: barrier.cvl |
| 20 | $(VERIFY) -inputB=4 barrier.cvl | |
| 21 | ||
| [9fb69d3] | 22 | barrier2: barrier2.cvl |
| 23 | $(VERIFY) -inputB=4 barrier2.cvl | |
| 24 | ||
| [72c01cc] | 25 | # Two kinds of violations are found in the following: |
| 26 | # a deadlock, and an assertion violation: | |
| 27 | barrierBad: barrierBad.cvl | |
| [7e8e35c] | 28 | $(VERIFY) -inputB=4 -min barrierBad.cvl |
| 29 | $(CIVL) replay -id=0 barrierBad.cvl | |
| 30 | $(CIVL) replay -id=1 barrierBad.cvl | |
| [72c01cc] | 31 | |
| [9fb69d3] | 32 | blockAdder: blockAdder.cvl |
| 33 | $(VERIFY) -inputB=6 -inputW=3 blockAdder.cvl | |
| 34 | ||
| 35 | blockAdderBad: blockAdderBad.cvl | |
| [7e8e35c] | 36 | $(VERIFY) -inputB=6 -inputW=3 -min blockAdderBad.cvl |
| [9fb69d3] | 37 | $(CIVL) replay blockAdderBad.cvl |
| [72c01cc] | 38 | |
| 39 | dining: dining.cvl | |
| 40 | $(VERIFY) -inputB=4 dining.cvl | |
| 41 | ||
| [30cc8b7] | 42 | diningBad: |
| [7e8e35c] | 43 | $(VERIFY) -inputB=4 -min diningBad.cvl |
| [72c01cc] | 44 | $(CIVL) replay diningBad.cvl |
| 45 | ||
| [9fb69d3] | 46 | locksBad: locksBad.cvl |
| 47 | $(VERIFY) locksBad.cvl | |
| 48 | ||
| 49 | locksBad10: locksBad10.cvl | |
| 50 | $(VERIFY) locksBad10.cvl | |
| 51 | ||
| 52 | locksGood: locksGood.cvl | |
| 53 | $(VERIFY) locksGood.cvl | |
| 54 | ||
| 55 | spawn: spawn.cvl | |
| [7e8e35c] | 56 | $(VERIFY) -inputN=10 spawn.cvl |
| [9fb69d3] | 57 | |
| 58 | spawn2: spawn2.cvl | |
| [7e8e35c] | 59 | $(VERIFY) -inputN=10 spawn2.cvl |
| [9fb69d3] | 60 | |
| 61 | spawnBad: spawnBad.cvl | |
| [7e8e35c] | 62 | $(VERIFY) -inputN=10 spawnBad.cvl |
| [72c01cc] | 63 | |
| 64 | clean: | |
| 65 | rm -rf CIVLREP *~ | |
| 66 |
Note:
See TracBrowser
for help on using the repository browser.
