583 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Adam Chlipala	15a5235792	MessagesAndRefinement: add to README	2016-05-08 19:00:15 -04:00
Adam Chlipala	254f370544	MessagesAndRefinement chapter: a pass through it all	2016-05-08 18:59:36 -04:00
Adam Chlipala	6333420f53	MessagesAndRefinement chapter: more algebraic laws	2016-05-08 18:43:27 -04:00
Adam Chlipala	97e672a323	MessagesAndRefinement chapter: refinement	2016-05-08 18:16:59 -04:00
Adam Chlipala	c48cf684b0	MessagesAndRefinement chapter: object-language definition	2016-05-08 17:47:43 -04:00
Adam Chlipala	7a864f14df	MessagesAndRefinement: comments	2016-05-08 16:58:41 -04:00
Adam Chlipala	fdc5d2dee2	MessagesAndRefinement: gratuitous_composition_expanded	2016-05-08 15:56:15 -04:00
Adam Chlipala	012a3cc78a	MessagesAndRefinement: gratuitous_composition	2016-05-08 09:24:00 -04:00
Adam Chlipala	9806321af1	MessagesAndRefinement: refines_add2_with_tester	2016-05-07 21:43:06 -04:00
Adam Chlipala	137121dcdc	MessagesAndRefinement: refines_Par	2016-05-07 21:25:37 -04:00
Adam Chlipala	db7a355195	MessagesAndRefinement: refines_Dup	2016-05-07 19:22:12 -04:00
Adam Chlipala	86516a58ec	MessagesAndRefinement: add2_once_refines_simple_addN_once	2016-05-07 18:50:04 -04:00
Adam Chlipala	d18dc3044e	MessagesAndRefinement: trace refinement	2016-05-04 15:52:42 -04:00
Adam Chlipala	c3935ce842	MessagesAndRefinement: base syntax and semantics	2016-05-04 15:29:34 -04:00
Adam Chlipala	1cb930d8d1	Fixes for Coq 8.4	2016-05-01 20:09:39 -04:00
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	8c67fc5468	ConcurrentSeparationLogic chapter: proofreading	2016-04-29 17:37:17 -04:00
Adam Chlipala	2f1d28a36a	ConcurrentSeparationLogic chapter: soundness proof	2016-04-29 13:54:58 -04:00
Adam Chlipala	66ba12e539	ConcurrentSeparationLogic chapter: object language and program logic	2016-04-29 12:58:23 -04:00
Adam Chlipala	f933a3ceab	ConcurrentSeparationLogic: comments	2016-04-29 11:16:50 -04:00
Adam Chlipala	320eb45126	ConcurrentSeparationLogic: 3-stage producer-consumer	2016-04-28 10:20:16 -04:00
Adam Chlipala	6e80356fed	ConcurrentSeparationLogic: more automation in examples	2016-04-28 10:07:43 -04:00
Adam Chlipala	a242a93a7e	ConcurrentSeparationLogic: a producer-consumer example (after tweaking SepCancel)	2016-04-28 10:03:10 -04:00
Adam Chlipala	c335550a77	ConcurrentSeparationLogic: first example	2016-04-28 09:16:42 -04:00
Adam Chlipala	38d4e24966	ConcurrentSeparationLogic.v: finished soundness proof	2016-04-27 19:54:51 -04:00
Adam Chlipala	856d8b43b2	ConcurrentSeparationLogic: for soundness proof, only cases left are for unlock and parallel composition	2016-04-27 18:04:39 -04:00
Adam Chlipala	de4b8fbec2	ConcurrentSeparationLogic: defined a program logic	2016-04-27 14:10:56 -04:00
Adam Chlipala	e133afa3b8	Strengthen [sets] tactic	2016-04-26 20:52:39 -04:00
Adam Chlipala	132ac914e4	Sets: change parsing precedence	2016-04-26 13:46:48 -04:00
Adam Chlipala	512f585d90	SharedMemory: make work with Coq 8.5	2016-04-25 09:00:28 -04:00
Adam Chlipala	4744a4039c	SharedMemory chapter: proofreading	2016-04-24 22:19:03 -04:00
Adam Chlipala	c60ec5864b	SharedMemory chapter: proof of partial-order reduction	2016-04-24 21:23:46 -04:00
Adam Chlipala	5ee82091f7	SharedMemory chapter: local actions	2016-04-24 19:53:19 -04:00
Adam Chlipala	545f29c68d	SharedMemory chapter: more on operational semantics	2016-04-24 19:26:29 -04:00
Adam Chlipala	592c7207bc	SharedMemory chapter: operational semantics	2016-04-24 19:17:11 -04:00
Adam Chlipala	7675534511	SharedMemory: formatting cleanup	2016-04-24 15:31:34 -04:00
Adam Chlipala	9f938e6ac1	SharedMemory: comments	2016-04-24 15:29:21 -04:00
Adam Chlipala	8d250037e7	SharedMemory: prove that our running-time bound relation is not total	2016-04-24 14:38:05 -04:00
Adam Chlipala	9de4dbdebe	SharedMemory: model-checked a concrete program with partial-order reduction	2016-04-24 14:29:28 -04:00
Adam Chlipala	34f586559f	SharedMemory: soundness of partial-order reduction (or one particular flavor thereof)	2016-04-24 13:56:33 -04:00
Adam Chlipala	50baaa91fe	SharedMemory: for partial-order reduction, only admit left uses the crucial commutativity property	2016-04-24 13:01:16 -04:00
Adam Chlipala	ec5df8f782	SharedMemory: proved the easier case of step->stepC	2016-04-24 08:30:25 -04:00
Adam Chlipala	606efc383d	SharedMemory: formulated a strategy for proving partial-order reduction, based on completing each trace to a stuck state	2016-04-23 21:09:53 -04:00
Adam Chlipala	3b7d898b0f	SharedMemory: commutes_sound	2016-04-22 19:11:42 -04:00
Adam Chlipala	784c89332d	SharedMemory: independent_threads	2016-04-22 18:25:07 -04:00
Adam Chlipala	ec5a4a198e	SharedMemory: change StepParProceed	2016-04-22 17:58:14 -04:00
Adam Chlipala	e9849b9e9c	SharedMemory: stronger notAboutToFail	2016-04-21 20:35:34 -04:00
Adam Chlipala	a8a8ff0bc6	SharedMemory: first optimization	2016-04-21 19:12:02 -04:00
Adam Chlipala	f37e9ba34d	SharedMemory: model-checking example, after tweaking library	2016-04-21 13:42:30 -04:00