projects
/
model-checker.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
b81523a
)
model: replace list type with action_list_t
author
Brian Norris
<banorris@uci.edu>
Wed, 19 Sep 2012 02:29:05 +0000
(19:29 -0700)
committer
Brian Norris
<banorris@uci.edu>
Wed, 19 Sep 2012 02:29:05 +0000
(19:29 -0700)
model.cc
patch
|
blob
|
history
model.h
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index 52b2e17dce3cc0b637af399eab102e50879fe44a..ec99b9a745de0960087e1f4a4bd33aafa82a920c 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-30,7
+30,7
@@
ModelChecker::ModelChecker(struct model_params params) :
obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
promises(new std::vector<Promise *>()),
futurevalues(new std::vector<struct PendingFutureValue>()),
obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
promises(new std::vector<Promise *>()),
futurevalues(new std::vector<struct PendingFutureValue>()),
- lazy_sync_with_release(new HashTable<void *,
std::list<ModelAction *>
, uintptr_t, 4>()),
+ lazy_sync_with_release(new HashTable<void *,
action_list_t
, uintptr_t, 4>()),
thrd_last_action(new std::vector<ModelAction *>(1)),
node_stack(new NodeStack()),
mo_graph(new CycleGraph()),
thrd_last_action(new std::vector<ModelAction *>(1)),
node_stack(new NodeStack()),
mo_graph(new CycleGraph()),
@@
-1043,7
+1043,7
@@
void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *rel
complete = release_seq_head(rf, release_heads);
if (!complete) {
/* add act to 'lazy checking' list */
complete = release_seq_head(rf, release_heads);
if (!complete) {
/* add act to 'lazy checking' list */
-
std::list<ModelAction *>
*list;
+
action_list_t
*list;
list = lazy_sync_with_release->get_safe_ptr(act->get_location());
list->push_back(act);
(*lazy_sync_size)++;
list = lazy_sync_with_release->get_safe_ptr(act->get_location());
list->push_back(act);
(*lazy_sync_size)++;
@@
-1065,13
+1065,13
@@
void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *rel
*/
bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
{
*/
bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
{
-
std::list<ModelAction *>
*list;
+
action_list_t
*list;
list = lazy_sync_with_release->getptr(location);
if (!list)
return false;
bool updated = false;
list = lazy_sync_with_release->getptr(location);
if (!list)
return false;
bool updated = false;
-
std::list<ModelAction *>
::iterator it = list->begin();
+
action_list_t
::iterator it = list->begin();
while (it != list->end()) {
ModelAction *act = *it;
const ModelAction *rf = act->get_reads_from();
while (it != list->end()) {
ModelAction *act = *it;
const ModelAction *rf = act->get_reads_from();
diff --git
a/model.h
b/model.h
index eb50d371e2e1694c2d4494467a1bf7325524b925..fd6e6c234f1c4d55e9a9a17ac652484f28be53b2 100644
(file)
--- a/
model.h
+++ b/
model.h
@@
-163,7
+163,7
@@
private:
* This structure maps its lists by object location. Each ModelAction
* in the lists should be an acquire operation.
*/
* This structure maps its lists by object location. Each ModelAction
* in the lists should be an acquire operation.
*/
- HashTable<void *,
std::list<ModelAction *>
, uintptr_t, 4> *lazy_sync_with_release;
+ HashTable<void *,
action_list_t
, uintptr_t, 4> *lazy_sync_with_release;
/**
* Represents the total size of the
/**
* Represents the total size of the