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

2013-02-27	Brian Norris	model: bugfix - correct RR coherence for Promises	blob \| commitdiff \| raw \| diff to current
2013-02-27	Brian Norris	cyclegraph: change Promise nodes map	blob \| commitdiff \| raw \| diff to current
2013-02-26	Brian Norris	model: promises: eliminate threads when they "join"	blob \| commitdiff \| raw \| diff to current
2013-02-26	Brian Norris	model: bugfix - only allow promise satisfaction for...	blob \| commitdiff \| raw \| diff to current
2013-02-25	Brian Norris	threads: construct Thread only with a given "parent"	blob \| commitdiff \| raw \| diff to current
2013-02-25	Brian Demsky	repush changes	blob \| commitdiff \| raw \| diff to current
2013-02-25	Brian Demsky	fix conflicts	blob \| commitdiff \| raw \| diff to current
2013-02-25	Brian Demsky	fix norris mentioned bug	blob \| commitdiff \| raw \| diff to current
2013-02-25	Brian Norris	Revert "fix scheduling stuff to get nice round robin...	blob \| commitdiff \| raw \| diff to current
2013-02-25	Brian Demsky	fix scheduling stuff to get nice round robin scheduler...	blob \| commitdiff \| raw \| diff to current
2013-02-23	Brian Norris	model: bugfix - inherit future values from previous...	blob \| commitdiff \| raw \| diff to current
2013-02-23	Brian Norris	model: correct the "no valid reads" assertion	blob \| commitdiff \| raw \| diff to current
2013-02-22	Brian Norris	model: wake up pending (sleep-set) actions for fences	blob \| commitdiff \| raw \| diff to current
2013-02-21	Brian Norris	model: only backtrack fences when acquire is before...	blob \| commitdiff \| raw \| diff to current
2013-02-21	Brian Norris	model: document get_last{,_fence}_conflict()	blob \| commitdiff \| raw \| diff to current
2013-02-21	Brian Norris	model: schedule appropriate fence backtracking points	blob \| commitdiff \| raw \| diff to current
2013-02-21	Brian Norris	model: convert while-loops to for-loops	blob \| commitdiff \| raw \| diff to current
2013-02-20	Brian Norris	model: add 'const'	blob \| commitdiff \| raw \| diff to current
2013-02-16	Brian Norris	model: end-of-execution print	blob \| commitdiff \| raw \| diff to current
2013-02-16	Brian Norris	model: improve get_next_thread() comments	blob \| commitdiff \| raw \| diff to current
2013-02-15	Brian Norris	model: pull scheduler's thread selection into get_next_...	blob \| commitdiff \| raw \| diff to current
2013-02-15	Brian Norris	schedule: split Scheduler::next_thread() into separate...	blob \| commitdiff \| raw \| diff to current
2013-02-15	Brian Norris	model: factor out a 'switch_from_master()' function	blob \| commitdiff \| raw \| diff to current
2013-02-15	Brian Norris	model: rework the release sequence fixups	blob \| commitdiff \| raw \| diff to current
2013-02-15	Brian Norris	model: simple refactoring	blob \| commitdiff \| raw \| diff to current
2013-02-15	Brian Norris	model/threads: add documentation comments	blob \| commitdiff \| raw \| diff to current
2013-02-15	Brian Norris	model: fix leaking "pending actions"	blob \| commitdiff \| raw \| diff to current
2013-02-15	Brian Norris	model: add 'pending' assertion	blob \| commitdiff \| raw \| diff to current
2013-02-15	Brian Norris	model: stash all pending actions immediately	blob \| commitdiff \| raw \| diff to current
2013-02-15	Brian Norris	model: pull 'has_asserted()' check out of take_step()	blob \| commitdiff \| raw \| diff to current
2013-02-15	Brian Norris	threads: bugfix - do not call thread_current() from...	blob \| commitdiff \| raw \| diff to current
2013-02-15	Brian Norris	model: stash actions in each thread	blob \| commitdiff \| raw \| diff to current
2013-02-15	Brian Norris	model: return next thread from take_step()	blob \| commitdiff \| raw \| diff to current
2013-02-14	Brian Norris	threads/model: allocate Thread from w/in ModelChecker	blob \| commitdiff \| raw \| diff to current
2013-02-12	Brian Norris	model: set thread state during 'swap' calls	blob \| commitdiff \| raw \| diff to current
2013-02-12	Brian Norris	Merge branch 'fences'	blob \| commitdiff \| raw \| diff to current
2013-02-12	Brian Norris	model: prune may-read-from set early	blob \| commitdiff \| raw \| diff to current
2013-02-12	Brian Norris	model: rewrite mo_check_promises	blob \| commitdiff \| raw \| diff to current
2013-02-09	Brian Norris	model: remove argument from mo_check_promises	blob \| commitdiff \| raw \| diff to current
2013-02-09	Brian Norris	model: rename according to the comments	blob \| commitdiff \| raw \| diff to current
2013-02-07	Brian Norris	model: add read-write coherence for promise nodes	blob \| commitdiff \| raw \| diff to current
2013-02-06	Brian Norris	model: refactor to use a helper function	blob \| commitdiff \| raw \| diff to current
2013-02-06	Brian Norris	cyclegraph: fixup support for dumping the modification...	blob \| commitdiff \| raw \| diff to current
2013-02-06	Brian Norris	model: fully utilize Promise nodes in CycleGraph	blob \| commitdiff \| raw \| diff to current
2013-02-06	Brian Norris	model: cosmetic improvements to resolve_promises()	blob \| commitdiff \| raw \| diff to current
2013-02-06	Brian Norris	model: add write-to-promise edges	blob \| commitdiff \| raw \| diff to current
2013-02-06	Brian Norris	model: utilize CycleGraph 'addEdge()' status	blob \| commitdiff \| raw \| diff to current
2013-02-06	Brian Norris	model: add promise-node edges for 'read' actions	blob \| commitdiff \| raw \| diff to current
2013-02-06	Brian Norris	model: template-ize 'r_modification_order'	blob \| commitdiff \| raw \| diff to current
2013-02-06	Brian Norris	action: store Promise in ModelAction	blob \| commitdiff \| raw \| diff to current
2013-02-06	Brian Norris	model: don't print scheduler randomly	blob \| commitdiff \| raw \| diff to current
2013-01-29	Brian Norris	nodestack/model: spacing	blob \| commitdiff \| raw \| diff to current
2013-01-25	Brian Norris	cyclegraph: RMW atomicity violation must flag a cycle	blob \| commitdiff \| raw \| diff to current
2013-01-25	Brian Norris	model: remove ModelChecker::is_infeasible_ignoreRMW()	blob \| commitdiff \| raw \| diff to current
2013-01-24	Brian Norris	model: add immediate future value for RMW reordering	blob \| commitdiff \| raw \| diff to current
2013-01-24	Brian Norris	model: modify promises on THREAD_{CREATE,FINISH}	blob \| commitdiff \| raw \| diff to current
2013-01-24	Brian Norris	promise: associate Promises with a set of threads	blob \| commitdiff \| raw \| diff to current
2013-01-24	Brian Norris	action: record future value	blob \| commitdiff \| raw \| diff to current
2013-01-24	Brian Norris	future_value: add thread ID parameter	blob \| commitdiff \| raw \| diff to current
2013-01-24	Brian Norris	nodestack: pass 'struct future_value' to add_future_value()	blob \| commitdiff \| raw \| diff to current
2013-01-24	Brian Norris	model: add const to get_thread(ModelAction *act)	blob \| commitdiff \| raw \| diff to current
2013-01-24	Brian Norris	model: fixup indentation, spelling in comment	blob \| commitdiff \| raw \| diff to current
2013-01-24	Brian Norris	model: style	blob \| commitdiff \| raw \| diff to current
2013-01-24	Brian Norris	model: remove local variable	blob \| commitdiff \| raw \| diff to current
2013-01-23	Brian Norris	promise: rename has_sync_thread() -> thread_is_eliminated()	blob \| commitdiff \| raw \| diff to current
2013-01-23	Brian Norris	promise: rename check_promise() -> has_failed()	blob \| commitdiff \| raw \| diff to current
2013-01-23	Brian Norris	promise: rename increment_threads() -> eliminate_thread()	blob \| commitdiff \| raw \| diff to current
2013-01-23	Brian Norris	promise: construct with a 'future_value' struct	blob \| commitdiff \| raw \| diff to current
2013-01-23	Brian Norris	nodestack: pass writer ModelAction to add_future_value()	blob \| commitdiff \| raw \| diff to current
2013-01-23	Brian Norris	nodestack: eliminate get_future_value_expiration()	blob \| commitdiff \| raw \| diff to current
2013-01-23	Brian Demsky	fix bug in promise handling code...	blob \| commitdiff \| raw \| diff to current
2013-01-17	Brian Norris	model: bugfix - sleep sets are NOT directly compatible...	blob \| commitdiff \| raw \| diff to current
2013-01-10	Brian Norris	model: reformat execution trace prints	blob \| commitdiff \| raw \| diff to current
2013-01-10	Brian Norris	model: spelling mistake	blob \| commitdiff \| raw \| diff to current
2013-01-10	Brian Norris	model: fixup "infeasible" messages	blob \| commitdiff \| raw \| diff to current
2013-01-08	Brian Norris	model: add 'add_future_value()' wrapper	blob \| commitdiff \| raw \| diff to current
2013-01-08	Brian Norris	model: add PendingFutureValue constructor	blob \| commitdiff \| raw \| diff to current
2013-01-03	Brian Norris	snapshot: turn C++ interface into C interface	blob \| commitdiff \| raw \| diff to current
2013-01-02	Brian Norris	action: add get_thread_operand() method	blob \| commitdiff \| raw \| diff to current
2013-01-02	Brian Norris	model: use get_thread(curr) instead of get_current_thread()	blob \| commitdiff \| raw \| diff to current
2012-12-18	Brian Norris	model: refactor check_current_action, next thread compu...	blob \| commitdiff \| raw \| diff to current
2012-12-15	Brian Norris	clean up some DEBUG() messages	blob \| commitdiff \| raw \| diff to current
2012-12-13	Brian Norris	model: check for NULL parent Node	blob \| commitdiff \| raw \| diff to current
2012-12-13	Brian Norris	model: use helper 'get_thread()'	blob \| commitdiff \| raw \| diff to current
2012-12-13	Brian Norris	model: style fixups	blob \| commitdiff \| raw \| diff to current
2012-12-13	Brian Norris	model: add 'set_latest_backtrack()'	blob \| commitdiff \| raw \| diff to current
2012-12-13	Brian Norris	model: print bug reports only for feasible executions	blob \| commitdiff \| raw \| diff to current
2012-12-13	Brian Norris	model: bugfix - mo_may_allow was too restrictive	blob \| commitdiff \| raw \| diff to current
2012-12-13	Brian Norris	model: make dumpGraph 'const'	blob \| commitdiff \| raw \| diff to current
2012-12-13	Brian Norris	model: remove snapshotted 'nextThread'	blob \| commitdiff \| raw \| diff to current
2012-12-13	Brian Norris	model: pass current action as function argument	blob \| commitdiff \| raw \| diff to current
2012-12-13	Brian Norris	model: simplify take_step()	blob \| commitdiff \| raw \| diff to current
2012-12-13	Brian Norris	model: force first thread to run immediately	blob \| commitdiff \| raw \| diff to current
2012-12-13	Brian Norris	model: change guaranteed condition into ASSERT()	blob \| commitdiff \| raw \| diff to current
2012-12-13	Brian Norris	model: spacing	blob \| commitdiff \| raw \| diff to current
2012-12-12	Brian Norris	model: rename 'promise_index' to 'i'	blob \| commitdiff \| raw \| diff to current
2012-12-12	Brian Norris	model: return value from switch_to_master	blob \| commitdiff \| raw \| diff to current
2012-12-08	Brian Norris	spacing	blob \| commitdiff \| raw \| diff to current
2012-12-07	Brian Norris	model: don't create UNINIT actions for Threads, mutexes...	blob \| commitdiff \| raw \| diff to current
2012-12-07	Brian Norris	model/action: bugfix - UNINIT actions do not have a...	blob \| commitdiff \| raw \| diff to current
next

C++11 memory model checker

RSS Atom