model: stash all pending actions immediately
[c11tester.git] / model.cc
2013-02-15 Brian Norrismodel: stash all pending actions immediately
2013-02-15 Brian Norrismodel: pull 'has_asserted()' check out of take_step()
2013-02-15 Brian Norristhreads: bugfix - do not call thread_current() from...
2013-02-15 Brian Norrismodel: stash actions in each thread
2013-02-15 Brian Norrismodel: return next thread from take_step()
2013-02-14 Brian Norristhreads/model: allocate Thread from w/in ModelChecker
2013-02-12 Brian Norrismodel: set thread state during 'swap' calls
2013-02-12 Brian NorrisMerge branch 'fences'
2013-02-12 Brian Norrismodel: prune may-read-from set early
2013-02-12 Brian Norrismodel: rewrite mo_check_promises
2013-02-09 Brian Norrismodel: remove argument from mo_check_promises
2013-02-09 Brian Norrismodel: rename according to the comments
2013-02-07 Brian Norrismodel: add read-write coherence for promise nodes
2013-02-06 Brian Norrismodel: refactor to use a helper function
2013-02-06 Brian Norriscyclegraph: fixup support for dumping the modification...
2013-02-06 Brian Norrismodel: fully utilize Promise nodes in CycleGraph
2013-02-06 Brian Norrismodel: cosmetic improvements to resolve_promises()
2013-02-06 Brian Norrismodel: add write-to-promise edges
2013-02-06 Brian Norrismodel: utilize CycleGraph 'addEdge()' status
2013-02-06 Brian Norrismodel: add promise-node edges for 'read' actions
2013-02-06 Brian Norrismodel: template-ize 'r_modification_order'
2013-02-06 Brian Norrisaction: store Promise in ModelAction
2013-02-06 Brian Norrismodel: don't print scheduler randomly
2013-01-29 Brian Norrisnodestack/model: spacing
2013-01-25 Brian Norriscyclegraph: RMW atomicity violation must flag a cycle
2013-01-25 Brian Norrismodel: remove ModelChecker::is_infeasible_ignoreRMW()
2013-01-24 Brian Norrismodel: add immediate future value for RMW reordering
2013-01-24 Brian Norrismodel: modify promises on THREAD_{CREATE,FINISH}
2013-01-24 Brian Norrispromise: associate Promises with a set of threads
2013-01-24 Brian Norrisaction: record future value
2013-01-24 Brian Norrisfuture_value: add thread ID parameter
2013-01-24 Brian Norrisnodestack: pass 'struct future_value' to add_future_value()
2013-01-24 Brian Norrismodel: add const to get_thread(ModelAction *act)
2013-01-24 Brian Norrismodel: fixup indentation, spelling in comment
2013-01-24 Brian Norrismodel: style
2013-01-24 Brian Norrismodel: remove local variable
2013-01-23 Brian Norrispromise: rename has_sync_thread() -> thread_is_eliminated()
2013-01-23 Brian Norrispromise: rename check_promise() -> has_failed()
2013-01-23 Brian Norrispromise: rename increment_threads() -> eliminate_thread()
2013-01-23 Brian Norrispromise: construct with a 'future_value' struct
2013-01-23 Brian Norrisnodestack: pass writer ModelAction to add_future_value()
2013-01-23 Brian Norrisnodestack: eliminate get_future_value_expiration()
2013-01-23 Brian Demskyfix bug in promise handling code...
2013-01-17 Brian Norrismodel: bugfix - sleep sets are NOT directly compatible...
2013-01-10 Brian Norrismodel: reformat execution trace prints
2013-01-10 Brian Norrismodel: spelling mistake
2013-01-10 Brian Norrismodel: fixup "infeasible" messages
2013-01-08 Brian Norrismodel: add 'add_future_value()' wrapper
2013-01-08 Brian Norrismodel: add PendingFutureValue constructor
2013-01-03 Brian Norrissnapshot: turn C++ interface into C interface
2013-01-02 Brian Norrisaction: add get_thread_operand() method
2013-01-02 Brian Norrismodel: use get_thread(curr) instead of get_current_thread()
2012-12-18 Brian Norrismodel: refactor check_current_action, next thread compu...
2012-12-15 Brian Norrisclean up some DEBUG() messages
2012-12-13 Brian Norrismodel: check for NULL parent Node
2012-12-13 Brian Norrismodel: use helper 'get_thread()'
2012-12-13 Brian Norrismodel: style fixups
2012-12-13 Brian Norrismodel: add 'set_latest_backtrack()'
2012-12-13 Brian Norrismodel: print bug reports only for feasible executions
2012-12-13 Brian Norrismodel: bugfix - mo_may_allow was too restrictive
2012-12-13 Brian Norrismodel: make dumpGraph 'const'
2012-12-13 Brian Norrismodel: remove snapshotted 'nextThread'
2012-12-13 Brian Norrismodel: pass current action as function argument
2012-12-13 Brian Norrismodel: simplify take_step()
2012-12-13 Brian Norrismodel: force first thread to run immediately
2012-12-13 Brian Norrismodel: change guaranteed condition into ASSERT()
2012-12-13 Brian Norrismodel: spacing
2012-12-12 Brian Norrismodel: rename 'promise_index' to 'i'
2012-12-12 Brian Norrismodel: return value from switch_to_master
2012-12-08 Brian Norrisspacing
2012-12-07 Brian Norrismodel: don't create UNINIT actions for Threads, mutexes...
2012-12-07 Brian Norrismodel/action: bugfix - UNINIT actions do not have a...
2012-12-07 Brian Norrismodel: remove old "uninitialized" bug check
2012-12-07 Brian Norrismodel: generate UNINIT actions as new atomic operations...
2012-12-07 Brian Norrismodel: add helper for allocating new UNINIT actions
2012-12-07 Brian Norrismodel: clear a ModelAction's reads-from properly
2012-12-06 Brian Norrismodel: refactoring + spacing
2012-12-05 Brian Norrismodel: stop thread-trace search once edge is added
2012-12-05 Brian Norrismodel: fix bugs in fence-acquire synchronization
2012-12-04 Brian Norrismodel: add process_fence()
2012-12-04 Brian Norrismodel: distinguish between 'read' and 'acquire' in...
2012-12-04 Brian Norrismodel: add read-acquire/fence-release support
2012-12-04 Brian Norrismodel: privatize a few interfaces
2012-12-04 Brian Norrismodel/action: move complicated read_from logic into...
2012-12-04 Brian Norrismodel: record last fence-release from each thread
2012-12-04 Brian Norrismodel: remove extraneous copy-and-paste
2012-12-04 Brian Norrismodel: add seq-cst fence rules
2012-12-04 Brian Norrisaction/model: backtrack for seq-cst and release/acquire...
2012-12-03 Brian Norrismodel: refactor build_reads_from_past
2012-12-03 Brian Norrismodel: add get_last_seq_cst_fence
2012-12-03 Brian Norrismodel: rename last_seq_cst -> last_sc_write
2012-12-01 Brian Norrismodel: rename get_last_seq_cst -> get_last_seq_cst_write
2012-11-20 Brian Norrismodel: add const
2012-11-20 Brian Norrisschedule: rename get_enabled() -> get_enabled_array()
2012-11-20 Brian Norrismodel: rename isfinalfeasible -> is_feasible_prefix_ign...
2012-11-20 Brian Norrismodel: replace isfinalfeasible() with stronger check
2012-11-20 Brian Norrismodel: privatize, move isfinalfeasible()
2012-11-20 Brian Norrismodel: rename some 'isfeasible...' functions to 'is_inf...
2012-11-20 Brian Norrismodel: privatize some functions
2012-11-20 Brian Norrismain/model: move full user-program execution to ModelCh...
next