Fixes

Add sleep score

Little adjustment

Fix bug

Add an exit node in predicate trees

Design a method to select predicate branches based on exploration counts

Avoid using a HashTable to associate FuncInsts with ModelActions; a slight improvement in performance

Turns out that calling Predicate::evaluate in FuncNode::follow_branch and NewFuzzer::prune_writes slows down the fuzzer

Performance fix; delete unused data structures

Select a new predicate branch when the selected branch in the predicate tree fails and the failed thread can not find any other thread to wait for

Some edits

Toward implementing the counter approach to monitor threads

Monitor threads when they enter functions and decide if others (if there is any) should keep waiting for them

Add some documentation for WaitObj

BFS with distance was not implemented correctly

Fix a bug

Every time a thread enters a function, check whether other threads should still wait for this thread or not.

Fix methods

Add some methods for WaitObj

Create WaitObj to store information about which thread is waiting for whom and is waiting by whom

Add default memory allocation and free functions for HSIterator and some other tiny stuff

Compute the threads that a paused thread my wait for

Toward computing which threads a paused thread may wait for

Do not unset FuncInst locations when new executions start; check if execution numbers match instead

Reorganize codes

Move one snapshotted data structure from ModelHistory to ModelExecution

Fix a memory bug

Free memory

Notify threads paused by the Fuzzer when the desired write is available

Clear headers

Change the return type of Predicate::evaluate

Concrete predicate class

Factor predicate expression types into a separate file

Able to evaluate predicate expression against a 'context' and generate concrete predicates

Need to free memory

Fix a bug

Fix a bug in pthread_mutex_unlock; initialize mutex if necessary when pthread_mutex_timedlock is called

Keep track of which FuncNodes may write to a memory location

Add comment about the difference between ModelAction::is_write and FuncInst::is_write

Construct the graph of methods based on the order that methods are called, rather than construct it as a call graph

Add edges between FuncNodes

Change action_list_buffer to snapshot memory instead of half-shapshot-half-non-snapshot

Make sure that actions that do writes are labeled correctly in predicate trees

Reorganize codes

Add atomic write actions to predicate trees

Remove an unused data structure

Remove unused codes

Modify the implementation of wait and timed wait operation

Do not process read actions paused by the fuzzer

seems to work

When an atomic read action cannot read from a desired write, make this thread sleep; half working now, still got some bug to fix

split add_action_to_lists into to two functions and change the order of how things are processed in check_current_action

remove a redundant member function that I added before

fix bug by changing MEMALLOC to SNAPSHOTALLOC

improve efficiency of selectWrite

remove unused member functions

move codes around in history.cc, and NewFuzzer::selectWrite is half working

remove unused member functions and add a new data structure

only select a new predicate branch when new read actions are processed

some edits to NewFuzzer

performace fix

fix bug

add a data structrue to keep track of the run-time position in the predicate tree for each thread

initial commit for declaring member functions of Fuzzer as virtual

only generate NULLITY predicate when it has ever been NULL; able to amend predicates that contain no predicate expressions

get rid of an unused function

restructure the codes that generate predicates

restructure code and working on deconstructors

experiment with generating equality predicates across memory locations; it seems to work, but codes can be reorganized

deduce which locations may share the same value from val_loc_map

update FuncNodes when there is a write

add helper functions; prepare for computing which memory locations may store the same values

Merge branch 'master' into branch-weiyu

allow ModelHistory to process non-atomic actions when they are created

reset memory locations of FuncInsts when new executions start

Add mailing list

Remove msqueue test case

Fix compile and readme

memory locations should not outlive executions

change the way to detect loops

defer the initial update of predicate tree for a better quality tree; generate nullity predicates when new Predicate nodes are created instead of changing unset predicates to nullity later

try to infer nullity predicate inside update_predicate_tree. Maybe rethink about the way to check back edges

change the structure of predicate expressions, and modify the way nullity predicates are added

experiment with adding NULLITY predicate

do optimization for FuncNode::update_tree

revert commit

fix a bug about get_reads_from_value

get rid of read_val_map; A bug is discovered.

fix bug - 'backedge' in predicate.cc uninitialized

fix bug

add a dummy predicate entry node to make code simpler; back edges are also added

restructrue code of funcnode.cc, and planning for adding back edges in predicate tree

Split FuncNode::get_or_add_inst into two separate functions.  Call add_inst inside process_action so that func_insts corresponding to ATOMIC RMWRCAS actions are created before those actions are converted to ATOMIC RMWR or ATOMIC READ

move modelhistory code back

toward updating predicate trees every time a function exits

move the codes that add actions to thrd_func_act_lists from history.cc to ModelExecution::add_action_to_lists

fix a bug and print predicate tree in xdot syntax

toward building a naive predicate tree

add print

move code around