| 2013-03-06 |
Brian Norris | model: don't print 'uninitialized' ModelActions in...
|
commit | commitdiff | tree |
| 2013-03-06 |
Brian Norris | impatomic: fences linker error
|
commit | commitdiff | tree |
| 2013-03-05 |
Brian Norris | Makefile: use $+ variable
|
commit | commitdiff | tree |
| 2013-03-05 |
Brian Norris | cyclegraph: memory "leak", fixup
|
commit | commitdiff | tree |
| 2013-03-05 |
Brian Norris | model: refactor the get_thread() selection
|
commit | commitdiff | tree |
| 2013-03-04 |
Brian Norris | refactor DBG_ENABLED() vs. verbose
|
commit | commitdiff | tree |
| 2013-03-04 |
Brian Norris | model: add promise printing to execution summaries
|
commit | commitdiff | tree |
| 2013-03-04 |
Brian Norris | nodestack: print thread status info in Node::print
|
commit | commitdiff | tree |
| 2013-03-04 |
Brian Norris | cyclegraph: missing form of checkReachable()
|
commit | commitdiff | tree |
| 2013-03-03 |
Brian Norris | model: rename check_deadlock() to is_circular_wait()
|
commit | commitdiff | tree |
| 2013-03-03 |
Brian Norris | model: add improved (?) deadlock detection
|
commit | commitdiff | tree |
| 2013-03-03 |
Brian Norris | threads: add waiting_on()
|
commit | commitdiff | tree |
| 2013-03-03 |
Brian Norris | mutex: change 'islocked' to hold Thread pointer
|
commit | commitdiff | tree |
| 2013-03-03 |
Brian Norris | action: add get_mutex()
|
commit | commitdiff | tree |
| 2013-03-03 |
Brian Norris | mutex: fix indentation
|
commit | commitdiff | tree |
| 2013-03-03 |
Brian Norris | action: add get_return_value()
|
commit | commitdiff | tree |
| 2013-03-02 |
Brian Norris | model: use get_write_value()
|
commit | commitdiff | tree |
| 2013-03-02 |
Brian Norris | model: bugfix - adding a Promise reader can cause failure
|
commit | commitdiff | tree |
| 2013-03-02 |
Brian Norris | model: hack dumpGraph() bug by "leaking" promises
|
commit | commitdiff | tree |
| 2013-03-02 |
Brian Norris | cyclegraph: simplify resolvePromise / mergeNodes
|
commit | commitdiff | tree |
| 2013-03-02 |
Brian Norris | model: refactor process_read logic
|
commit | commitdiff | tree |
| 2013-03-02 |
Brian Norris | check_recency: update/add documentation comments
|
commit | commitdiff | tree |
| 2013-03-02 |
Brian Norris | check_recency: improve templates, use when reading...
|
commit | commitdiff | tree |
| 2013-03-02 |
Brian Norris | check_recency: refactor some more, + include Promises
|
commit | commitdiff | tree |
| 2013-03-02 |
Brian Norris | check_recency: return a boolean status
|
commit | commitdiff | tree |
| 2013-03-02 |
Brian Norris | check_recency: only allow newer stores to "overwrite"
|
commit | commitdiff | tree |
| 2013-03-02 |
Brian Norris | check_recency: implement loops as function ModelAction...
|
commit | commitdiff | tree |
| 2013-03-02 |
Brian Norris | nodestack: add support functions for check_recency...
|
commit | commitdiff | tree |
| 2013-03-02 |
Brian Norris | model: check_recency: convert a few things to ASSERT()
|
commit | commitdiff | tree |
| 2013-03-02 |
Brian Norris | model: check_recency: fix indentation, spelling, comments
|
commit | commitdiff | tree |
| 2013-03-02 |
Brian Norris | action: bugfix - reads-from value should be VALUE_NONE...
|
commit | commitdiff | tree |
| 2013-03-02 |
Brian Norris | model: fixes for future value passing
|
commit | commitdiff | tree |
| 2013-03-02 |
Brian Norris | model: we only resolve one promise at a time
|
commit | commitdiff | tree |
| 2013-03-01 |
Brian Norris | model: fix ASSERT()
|
commit | commitdiff | tree |
| 2013-03-01 |
Brian Norris | promise: add 'same_value' helper, force value-checking...
|
commit | commitdiff | tree |
| 2013-03-01 |
Brian Norris | promise: bugfix - don't check value, check location
|
commit | commitdiff | tree |
| 2013-03-01 |
Brian Norris | action: add get_write_value()
|
commit | commitdiff | tree |
| 2013-03-01 |
Brian Norris | action: add ModelAction::get_reads_from_value()
|
commit | commitdiff | tree |
| 2013-03-01 |
Brian Norris | action, model: add ASSERT(), not NULL checks
|
commit | commitdiff | tree |
| 2013-03-01 |
Brian Norris | cyclegraph/model: unify, clean up graph printing
|
commit | commitdiff | tree |
| 2013-03-01 |
Brian Norris | nodestack: get_read_from_promise() never returns NULL
|
commit | commitdiff | tree |
| 2013-02-28 |
Brian Norris | model/schedule: comput "reduadant" measurement, print...
|
commit | commitdiff | tree |
| 2013-02-28 |
Brian Norris | cyclegraph: clean up mo_graph dump
|
commit | commitdiff | tree |
| 2013-02-28 |
Brian Norris | action: print promise number, not just ?
|
commit | commitdiff | tree |
| 2013-02-28 |
Brian Norris | nodestack: bugfix - clear backtracking properly
|
commit | commitdiff | tree |
| 2013-02-28 |
Brian Norris | promise: record multiple readers in the same Promise
|
commit | commitdiff | tree |
| 2013-02-28 |
Brian Norris | un-'const' some Promises
|
commit | commitdiff | tree |
| 2013-02-28 |
Brian Norris | nodestack: rewrite promise-resolution "counting"
|
commit | commitdiff | tree |
| 2013-02-28 |
Brian Norris | model: hook up 'read-from-promise' backtracking in...
|
commit | commitdiff | tree |
| 2013-02-28 |
Brian Norris | nodestack: add read_from_promises backtracking
|
commit | commitdiff | tree |
| 2013-02-28 |
Brian Norris | nodestack: bugfix - rewrite 'may-read-from' and 'future...
|
commit | commitdiff | tree |
| 2013-02-28 |
Brian Norris | model: shorten some code
|
commit | commitdiff | tree |
| 2013-02-28 |
Brian Norris | model: rename 'reads_from' to 'rf'
|
commit | commitdiff | tree |
| 2013-02-28 |
Brian Norris | nodestack: rename 'read_from' to 'read_from_past'
|
commit | commitdiff | tree |
| 2013-02-28 |
Brian Norris | model: don't call process_read() for 2nd half of RMW...
|
commit | commitdiff | tree |
| 2013-02-27 |
Brian Norris | model: bugfix - correct the "equality" check for RR...
|
commit | commitdiff | tree |
| 2013-02-27 |
Brian Norris | cyclegraph: bugfix - allow to compile with SUPPORT_MOD_ORDER...
|
commit | commitdiff | tree |
| 2013-02-27 |
Brian Norris | model: bugfix - correct RR coherence for Promises
|
commit | commitdiff | tree |
| 2013-02-27 |
Brian Norris | cyclegraph: change Promise nodes map
|
commit | commitdiff | tree |
| 2013-02-26 |
Brian Norris | model: promises: eliminate threads when they "join"
|
commit | commitdiff | tree |
| 2013-02-26 |
Brian Norris | schedule: remove commented-out code
|
commit | commitdiff | tree |
| 2013-02-26 |
Brian Norris | model: bugfix - only allow promise satisfaction for...
|
commit | commitdiff | tree |
| 2013-02-25 |
Brian Norris | threads: construct Thread only with a given "parent"
|
commit | commitdiff | tree |
| 2013-02-25 |
Brian Norris | Revert "fix scheduling stuff to get nice round robin...
|
commit | commitdiff | tree |
| 2013-02-23 |
Brian Norris | nodestack: bugfix - reset backtracking points on diverging...
|
commit | commitdiff | tree |
| 2013-02-23 |
Brian Norris | model: bugfix - inherit future values from previous...
|
commit | commitdiff | tree |
| 2013-02-23 |
Brian Norris | nodestack: don't use C++ references
|
commit | commitdiff | tree |
| 2013-02-23 |
Brian Norris | model: correct the "no valid reads" assertion
|
commit | commitdiff | tree |
| 2013-02-23 |
Brian Norris | promise: stash the whole future_value
|
commit | commitdiff | tree |
| 2013-02-22 |
Brian Norris | test: fences: add simple, semi-useful fence tests
|
commit | commitdiff | tree |
| 2013-02-22 |
Brian Norris | test: add double-read-fv
|
commit | commitdiff | tree |
| 2013-02-22 |
Brian Norris | action: backtrack/sleep-sets for seq-cst fences
|
commit | commitdiff | tree |
| 2013-02-22 |
Brian Norris | model: wake up pending (sleep-set) actions for fences
|
commit | commitdiff | tree |
| 2013-02-21 |
Brian Norris | model: only backtrack fences when acquire is before...
|
commit | commitdiff | tree |
| 2013-02-21 |
Brian Norris | model: document get_last{,_fence}_conflict()
|
commit | commitdiff | tree |
| 2013-02-21 |
Brian Norris | model: schedule appropriate fence backtracking points
|
commit | commitdiff | tree |
| 2013-02-21 |
Brian Norris | model: convert while-loops to for-loops
|
commit | commitdiff | tree |
| 2013-02-20 |
Brian Norris | model: add 'const'
|
commit | commitdiff | tree |
| 2013-02-20 |
Brian Norris | include: fixup header inclusion
|
commit | commitdiff | tree |
| 2013-02-20 |
Brian Norris | don't include action.h from model.h
|
commit | commitdiff | tree |
| 2013-02-20 |
Brian Norris | model/action: move action_list_t to model.h
|
commit | commitdiff | tree |
| 2013-02-20 |
Brian Norris | promise: move constructor out of header
|
commit | commitdiff | tree |
| 2013-02-16 |
Brian Norris | scheduler: refactor round-robin loop
|
commit | commitdiff | tree |
| 2013-02-16 |
Brian Norris | model: end-of-execution print
|
commit | commitdiff | tree |
| 2013-02-16 |
Brian Norris | model: improve get_next_thread() comments
|
commit | commitdiff | tree |
| 2013-02-15 |
Brian Norris | schedule: simplify Scheduler::select_next_thread()
|
commit | commitdiff | tree |
| 2013-02-15 |
Brian Norris | model: pull scheduler's thread selection into get_next_thread()
|
commit | commitdiff | tree |
| 2013-02-15 |
Brian Norris | schedule: split Scheduler::next_thread() into separate...
|
commit | commitdiff | tree |
| 2013-02-15 |
Brian Norris | model: factor out a 'switch_from_master()' function
|
commit | commitdiff | tree |
| 2013-02-15 |
Brian Norris | model: rework the release sequence fixups
|
commit | commitdiff | tree |
| 2013-02-15 |
Brian Norris | model: simple refactoring
|
commit | commitdiff | tree |
| 2013-02-15 |
Brian Norris | model/threads: add documentation comments
|
commit | commitdiff | tree |
| 2013-02-15 |
Brian Norris | model: fix leaking "pending actions"
|
commit | commitdiff | tree |
| 2013-02-15 |
Brian Norris | model: add 'pending' assertion
|
commit | commitdiff | tree |
| 2013-02-15 |
Brian Norris | model: stash all pending actions immediately
|
commit | commitdiff | tree |
| 2013-02-15 |
Brian Norris | model: pull 'has_asserted()' check out of take_step()
|
commit | commitdiff | tree |
| 2013-02-15 |
Brian Norris | threads: bugfix - do not call thread_current() from...
|
commit | commitdiff | tree |
| 2013-02-15 |
Brian Norris | model: stash actions in each thread
|
commit | commitdiff | tree |
| 2013-02-15 |
Brian Norris | model: return next thread from take_step()
|
commit | commitdiff | tree |
| 2013-02-14 |
Brian Norris | threads/model: allocate Thread from w/in ModelChecker
|
commit | commitdiff | tree |
| next |
projects / model-checker.git / search