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