Programming Languages Research Group: Git - model-checker.git/history

2012-11-01	Brian Demsky	found the bug	blob \| commitdiff \| raw
2012-11-01	Brian Demsky	fix new bug	blob \| commitdiff \| raw \| diff to current
2012-11-01	Brian Norris	model: silence "uninitialized" warning	blob \| commitdiff \| raw \| diff to current
2012-11-01	Brian Norris	model: update mo_may_allow restrictions	blob \| commitdiff \| raw \| diff to current
2012-10-26	Brian Demsky	changes to allow running programs with racing initializ...	blob \| commitdiff \| raw \| diff to current
2012-10-25	Brian Demsky	embarrassing bug...fixed...	blob \| commitdiff \| raw \| diff to current
2012-10-19	Brian Norris	model: fix - RMW cannot break release sequences	blob \| commitdiff \| raw \| diff to current
2012-10-12	Brian Demsky	forgot to add two files...	blob \| commitdiff \| raw \| diff to current
2012-10-12	Brian Demsky	commit untested condvar code	blob \| commitdiff \| raw \| diff to current
2012-10-12	Brian Demsky	Merge branch 'master' of ssh://demsky.eecs.uci.edu...	blob \| commitdiff \| raw \| diff to current
2012-10-11	Brian Norris	mutex: move mutex.h to standard name/location	blob \| commitdiff \| raw \| diff to current
2012-10-10	Brian Norris	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2012-10-10	Brian Demsky	make scheduler choose fair schedules when threads with...	blob \| commitdiff \| raw \| diff to current
2012-10-10	Brian Demsky	Merge branch 'master' of ssh://demsky.eecs.uci.edu...	blob \| commitdiff \| raw \| diff to current
2012-10-10	Brian Demsky	make linux_rw locks work again	blob \| commitdiff \| raw \| diff to current
2012-10-10	Brian Norris	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2012-10-10	Brian Demsky	fix some of the bugs related to barrier example...	blob \| commitdiff \| raw \| diff to current
2012-10-09	Brian Norris	rename threads.h -> threads-model.h	blob \| commitdiff \| raw \| diff to current
2012-10-09	Brian Demsky	did a little more looking at infeasible executions...	blob \| commitdiff \| raw \| diff to current
2012-10-09	Brian Norris	model: JOIN/LOCK unification	blob \| commitdiff \| raw \| diff to current
2012-10-09	Brian Demsky	mistake	blob \| commitdiff \| raw \| diff to current
2012-10-09	Brian Demsky	be much more careful about sending values backwards...	blob \| commitdiff \| raw \| diff to current
2012-10-08	Brian Demsky	be even more aggressive about sleep sets...	blob \| commitdiff \| raw \| diff to current
2012-10-08	Brian Norris	model: stack-allocated vector should use ModelAlloc	blob \| commitdiff \| raw \| diff to current
2012-10-08	Brian Norris	utilize SnapshotAlloc STL allocator	blob \| commitdiff \| raw \| diff to current
2012-10-08	Brian Norris	model: remove todo	blob \| commitdiff \| raw \| diff to current
2012-10-08	Brian Demsky	merge massive speedup with release sequence support...	blob \| commitdiff \| raw \| diff to current
2012-10-08	Brian Demsky	add support for sleep sets...	blob \| commitdiff \| raw \| diff to current
2012-10-08	Brian Norris	Merge branch 'norris'	blob \| commitdiff \| raw \| diff to current
2012-10-08	Brian Norris	model: add todo synchronization comment	blob \| commitdiff \| raw \| diff to current
2012-10-08	Brian Norris	model: be sure trace is "final feasible" before continu...	blob \| commitdiff \| raw \| diff to current
2012-10-08	Brian Norris	model: check data races during release sequence fixup	blob \| commitdiff \| raw \| diff to current
2012-10-08	Brian Norris	model: add release sequence model_thread ASSERT()	blob \| commitdiff \| raw \| diff to current
2012-10-08	Brian Norris	model: launch release sequence fixup actions when necessary	blob \| commitdiff \| raw \| diff to current
2012-10-08	Brian Norris	model: add special model-checker Thread to ModelChecker	blob \| commitdiff \| raw \| diff to current
2012-10-08	Brian Norris	model: add process_relseq_fixup()	blob \| commitdiff \| raw \| diff to current
2012-10-07	Brian Norris	model: wire up rest of release seq. resolution backtracking	blob \| commitdiff \| raw \| diff to current
2012-10-07	Brian Norris	model: disabled threads are "future ordered"	blob \| commitdiff \| raw \| diff to current
2012-10-07	Brian Norris	model: use proper size_t printf format	blob \| commitdiff \| raw \| diff to current
2012-10-05	Brian Demsky	1) more comments	blob \| commitdiff \| raw \| diff to current
2012-10-05	Brian Demsky	Merge branch 'master' of ssh://demsky.eecs.uci.edu...	blob \| commitdiff \| raw \| diff to current
2012-10-05	Brian Demsky	changes	blob \| commitdiff \| raw \| diff to current
2012-10-04	Brian Norris	model: remove unnecessary boolean variable	blob \| commitdiff \| raw \| diff to current
2012-10-04	Brian Norris	model: assign "pending" return values in release_seq_he...	blob \| commitdiff \| raw \| diff to current
2012-10-04	Brian Norris	model: update pending release sequence list type	blob \| commitdiff \| raw \| diff to current
2012-10-04	Brian Demsky	fix bug...can't mo_check_promises until we're done...	blob \| commitdiff \| raw \| diff to current
2012-10-04	Brian Demsky	local commit... bug that prunes too many executions	blob \| commitdiff \| raw \| diff to current
2012-10-04	Brian Demsky	Merge branch 'master' of /home/git/model-checker	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	action: remove clockvector flag from print() method	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	model: rename release_seq_head() -> release_seq_heads()	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	model: do not assume THREAD_FINISH is always the last...	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	fixup usage of int vs. thread_id_t	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	model: add const qualifier to get_thread()	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	model: rearrange conditionals, fixup take_step()	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	modeltypes: move small typedefs to own header	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	model: move get_thread() implementations out of header	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	model: move get_current_thread() implementation out...	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Demsky	Merge branch 'master' of /home/git/model-checker	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Demsky	a number of fixes to add missing mo_graph edges to...	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	model: update switch_to_master() comment	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Demsky	random memory leak fixes and memory access fixes	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	model: debug print - pending release sequences	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	(bug) revert JOIN/LOCK simplification	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	model: one release sequence may help resolve another	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	model: THREAD_FINISH triggers release sequence check	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Demsky	Merge branch 'master' of ssh://demsky.eecs.uci.edu...	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Demsky	a bug fix	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	assign sequence numbers after initial processing	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	model: remove obsolete ModelChecker::do_complete_join()	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	model: unify JOIN- and LOCK-related sleep/wake code	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	model: refactor mutex thread-blocking code	blob \| commitdiff \| raw \| diff to current
2012-10-03	Brian Norris	action: don't print clock vector when it is invalid	blob \| commitdiff \| raw \| diff to current
2012-10-02	Brian Norris	model: fix "earliest diverge" NULL pointer exception	blob \| commitdiff \| raw \| diff to current
2012-10-02	Brian Demsky	start support for drawing execution diagrams	blob \| commitdiff \| raw \| diff to current
2012-10-02	Brian Demsky	Fixed bug breaking our consolidation of future values...	blob \| commitdiff \| raw \| diff to current
2012-10-02	Brian Demsky	Two change:	blob \| commitdiff \| raw \| diff to current
2012-10-02	Brian Norris	model: refactor/reword initialize_curr_action()	blob \| commitdiff \| raw \| diff to current
2012-10-02	Brian Norris	model: always re-calculate clock vectors	blob \| commitdiff \| raw \| diff to current
2012-10-01	Brian Demsky	another bug fix	blob \| commitdiff \| raw \| diff to current
2012-10-01	Brian Demsky	bug fix...recompute promises of RMW actions at divergen...	blob \| commitdiff \| raw \| diff to current
2012-10-01	Brian Norris	model: utilize bad_synchronization flag	blob \| commitdiff \| raw \| diff to current
2012-10-01	Brian Norris	model: add "bad synchronization" flag	blob \| commitdiff \| raw \| diff to current
2012-10-01	Brian Norris	model: remove debug print	blob \| commitdiff \| raw \| diff to current
2012-09-29	Brian Demsky	missing commit of mo_graph changes	blob \| commitdiff \| raw \| diff to current
2012-09-28	Brian Demsky	fix bug from moving read_from check_recency...check_rec...	blob \| commitdiff \| raw \| diff to current
2012-09-27	Brian Norris	model: push mo_graph cycle check into release_seq code	blob \| commitdiff \| raw \| diff to current
2012-09-27	Brian Norris	model: add RMW violation debug print	blob \| commitdiff \| raw \| diff to current
2012-09-26	Brian Norris	model: avoid infinite loop in release_seq_head()	blob \| commitdiff \| raw \| diff to current
2012-09-26	Brian Norris	model: bugfix - iterator naming conflict	blob \| commitdiff \| raw \| diff to current
2012-09-26	Brian Norris	model: re-check release sequences after THREAD_JOIN	blob \| commitdiff \| raw \| diff to current
2012-09-26	Brian Norris	model: add current action work_queue comment	blob \| commitdiff \| raw \| diff to current
2012-09-25	Brian Norris	model: mutex synchronization -> re-check release sequences	blob \| commitdiff \| raw \| diff to current
2012-09-25	Brian Norris	model: trivial - rename 'updated' -> 'update'	blob \| commitdiff \| raw \| diff to current
2012-09-25	Brian Norris	model: bugfix - release sequences - handle Thread compl...	blob \| commitdiff \| raw \| diff to current
2012-09-25	Brian Norris	model: fixup spelling (and formatting) in comments	blob \| commitdiff \| raw \| diff to current
2012-09-25	Brian Norris	model: split THREAD_* processing into process_thread_ac...	blob \| commitdiff \| raw \| diff to current
2012-09-25	Brian Norris	Merge branch 'norris'	blob \| commitdiff \| raw \| diff to current
2012-09-25	Brian Norris	model: release_seq_head - rewrite RMW recursion as...	blob \| commitdiff \| raw \| diff to current
2012-09-25	Brian Demsky	add comments	blob \| commitdiff \| raw \| diff to current
next

C++11 memory model checker

RSS Atom