towards supporting scanalysis...
[model-checker.git] / scanalysis.cc
1 #include "scanalysis.h"
2 #include "action.h"
3 #include "threads-model.h"
4 #include "clockvector.h"
5
6 SCAnalysis::SCAnalysis() {
7         cvmap=new HashTable<const ModelAction *, ClockVector *, uintptr_t, 4>();
8 }
9
10 SCAnalysis::~SCAnalysis() {
11         delete(cvmap);
12 }
13
14 void SCAnalysis::analyze(action_list_t * actions) {
15         buildVectors(actions);
16         computeCV(actions);
17 }
18
19 void SCAnalysis::buildVectors(action_list_t *list) {
20         maxthreads=0;
21         for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
22                 ModelAction *act = *it;
23                 int threadid=id_to_int(act->get_tid());
24                 if (threadid > maxthreads)
25                         maxthreads=threadid;
26         }
27 }
28
29 bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) {
30         bool changed=false;
31
32         /* Merge in the clock vector from the write */
33         const ModelAction *write=read->get_reads_from();
34         ClockVector *writecv=cvmap->get(write);
35         changed|= ( writecv == NULL || cv->merge(writecv) && (*read < *write));
36
37         for(int i=0;i<=maxthreads;i++) {
38                 thread_id_t tid=int_to_id(i);
39                 if (tid==read->get_tid())
40                         continue;
41                 action_list_t * list=model->get_actions_on_obj(read->get_location(), tid);
42                 if (list==NULL)
43                         continue;
44                 for (action_list_t::reverse_iterator rit = list->rbegin(); rit != list->rend(); rit++) {
45                         ModelAction *write2 = *rit;
46                         ClockVector *write2cv = cvmap->get(write2);
47                         if (write2cv == NULL)
48                                 continue;
49                         
50                         /* write -sc-> write2 &&
51                                  write -rf-> R =>
52                                  R -sc-> write2 */
53                         if (write2cv->synchronized_since(write)) {
54                                 changed |= write2cv->merge(cv);
55                         }
56                 
57                         //looking for earliest write2 in iteration to satisfy this
58                         /* write2 -sc-> R &&
59                                  write -rf-> R =>
60                                  write2 -sc-> write */
61                         if (cv->synchronized_since(write2)) {
62                                 changed |= writecv == NULL || writecv->merge(write2cv);
63                                 break;
64                         }
65                 }
66         }
67         return changed;
68 }
69
70
71 void SCAnalysis::computeCV(action_list_t *list) {
72         bool changed=true;
73         bool firsttime=true;
74         ModelAction **last_act=(ModelAction **)model_calloc(1,(maxthreads+1)*sizeof(ModelAction *));
75         while(changed) {
76                 changed=changed&firsttime;
77                 firsttime=false;
78
79                 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
80                         ModelAction *act = *it;
81                         ModelAction *lastact = last_act[id_to_int(act->get_tid())];
82                         if (act->is_thread_start())
83                                 lastact=model->get_thread(act)->get_creation();
84                         ClockVector *lastcv=(lastact != NULL) ? cvmap->get(lastact) : NULL;
85                         last_act[id_to_int(act->get_tid())]=act;
86                         ClockVector *cv=cvmap->get(act);
87                         if ( cv == NULL ) {
88                                 cv = new ClockVector(lastcv, act);
89                                 cvmap->put(act, cv);
90                         } else if ( lastcv != NULL ) {
91                                         cv->merge(lastcv);
92                         }
93                         if (act->is_read()) {
94                                 changed|=processRead(act, cv);
95                         }
96                 }
97                 /* Reset the last action array */
98                 if (changed) {
99                         bzero(last_act, (maxthreads+1)*sizeof(ModelAction *));
100                 }
101         }
102         model_free(last_act);
103 }