Commit graph

8 commits

Author SHA1 Message Date
Adam Chlipala
daac5734b0 Finalizing ConcurrentSeparationLogic 2016-05-01 19:45:51 -04:00
Adam Chlipala
035bfa57ee Make SepCancel more conservative 2016-05-01 18:53:25 -04:00
Adam Chlipala
a242a93a7e ConcurrentSeparationLogic: a producer-consumer example (after tweaking SepCancel) 2016-04-28 10:03:10 -04:00
Adam Chlipala
47fd9a8abf SepCancel: adapt for Coq versions 2016-04-20 08:36:48 -04:00
Adam Chlipala
4209399eb1 Comment SeparationLogic, while getting it working with Coq 8.4 2016-04-19 21:25:39 -04:00
Adam Chlipala
c9d7a69287 SepCancel: now less conservative 2016-04-19 19:16:14 -04:00
Adam Chlipala
60c21c07ec SepCancel: be more cautious in a few ways 2016-04-19 18:36:25 -04:00
Adam Chlipala
e1844abf25 Factor out SepCancel 2016-04-19 14:28:30 -04:00