1 #include "scanalysis.h"
3 #include "threads-model.h"
4 #include "clockvector.h"
7 SCAnalysis::SCAnalysis() :
17 SCAnalysis::~SCAnalysis() {
20 void SCAnalysis::setExecution(ModelExecution * execution) {
21 this->execution=execution;
24 char * SCAnalysis::name() {
29 void SCAnalysis::print_list(action_list_t *list) {
30 model_print("---------------------------------------------------------------------\n");
32 model_print("Not SC\n");
33 unsigned int hash = 0;
35 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
36 const ModelAction *act = *it;
37 if (act->get_seq_number() > 0) {
38 if (badrfset.contains(act))
41 if (badrfset.contains(act)) {
42 model_print("Desired Rf: %u \n", badrfset.get(act)->get_seq_number());
45 hash = hash ^ (hash << 3) ^ ((*it)->hash());
47 model_print("HASH %u\n", hash);
48 model_print("---------------------------------------------------------------------\n");
51 void SCAnalysis::analyze(action_list_t *actions) {
52 action_list_t *list = generateSC(actions);
57 void SCAnalysis::check_rf(action_list_t *list) {
58 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
59 const ModelAction *act = *it;
61 if (act->get_reads_from() != lastwrmap.get(act->get_location()))
62 badrfset.put(act, lastwrmap.get(act->get_location()));
65 lastwrmap.put(act->get_location(), act);
69 bool SCAnalysis::merge(ClockVector *cv, const ModelAction *act, const ModelAction *act2) {
70 ClockVector *cv2 = cvmap.get(act2);
73 if (cv2->getClock(act->get_tid()) >= act->get_seq_number() && act->get_seq_number() != 0) {
75 //refuse to introduce cycles into clock vectors
79 return cv->merge(cv2);
82 int SCAnalysis::getNextActions(ModelAction ** array) {
85 for (int t = 0; t <= maxthreads; t++) {
86 action_list_t *tlt = &threadlists[t];
89 ModelAction *act = tlt->front();
90 ClockVector *cv = cvmap.get(act);
92 /* Find the earliest in SC ordering */
93 for (int i = 0; i <= maxthreads; i++) {
96 action_list_t *threadlist = &threadlists[i];
97 if (threadlist->empty())
99 ModelAction *first = threadlist->front();
100 if (cv->synchronized_since(first)) {
111 for (int t = 0; t <= maxthreads; t++) {
112 action_list_t *tlt = &threadlists[t];
115 ModelAction *act = tlt->front();
116 ClockVector *cv = act->get_cv();
118 /* Find the earliest in SC ordering */
119 for (int i = 0; i <= maxthreads; i++) {
122 action_list_t *threadlist = &threadlists[i];
123 if (threadlist->empty())
125 ModelAction *first = threadlist->front();
126 if (cv->synchronized_since(first)) {
136 ASSERT(count==0 || cyclic);
141 ModelAction * SCAnalysis::pruneArray(ModelAction **array,int count) {
146 /* Choose first non-write action */
147 ModelAction *nonwrite=NULL;
148 for(int i=0;i<count;i++) {
149 if (!array[i]->is_write())
150 if (nonwrite==NULL || nonwrite->get_seq_number() > array[i]->get_seq_number())
153 if (nonwrite != NULL)
156 /* Look for non-conflicting action */
157 ModelAction *nonconflict=NULL;
158 for(int a=0;a<count;a++) {
159 ModelAction *act=array[a];
160 for (int i = 0; i <= maxthreads && act != NULL; i++) {
161 thread_id_t tid = int_to_id(i);
162 if (tid == act->get_tid())
165 action_list_t *list = &threadlists[id_to_int(tid)];
166 for (action_list_t::iterator rit = list->begin(); rit != list->end(); rit++) {
167 ModelAction *write = *rit;
168 if (!write->is_write())
170 ClockVector *writecv = cvmap.get(write);
171 if (writecv->synchronized_since(act))
173 if (write->get_location() == act->get_location()) {
174 //write is sc after act
181 if (nonconflict == NULL || nonconflict->get_seq_number() > act->get_seq_number())
188 action_list_t * SCAnalysis::generateSC(action_list_t *list) {
189 int numactions=buildVectors(list);
192 action_list_t *sclist = new action_list_t();
193 ModelAction **array = (ModelAction **)model_calloc(1, (maxthreads + 1) * sizeof(ModelAction *));
194 int * choices = (int *) model_calloc(1, sizeof(int)*numactions);
199 int numActions = getNextActions(array);
202 ModelAction * act=pruneArray(array, numActions);
204 if (currchoice < endchoice) {
205 act = array[choices[currchoice]];
206 //check whether there is still another option
207 if ((choices[currchoice]+1)<numActions)
208 lastchoice=currchoice;
212 choices[currchoice]=0;
214 lastchoice=currchoice;
218 thread_id_t tid = act->get_tid();
220 threadlists[id_to_int(tid)].pop_front();
221 //add ordering constraints from this choice
222 if (updateConstraints(act)) {
223 //propagate changes if we have them
226 if (!prevc && cyclic) {
227 model_print("ROLLBACK in SC\n");
228 //check whether we have another choice
229 if (lastchoice != -1) {
230 //have to reset everything
231 choices[lastchoice]++;
232 endchoice=lastchoice+1;
244 sclist->push_back(act);
250 int SCAnalysis::buildVectors(action_list_t *list) {
253 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
254 ModelAction *act = *it;
256 int threadid = id_to_int(act->get_tid());
257 if (threadid > maxthreads) {
258 threadlists.resize(threadid + 1);
259 maxthreads = threadid;
261 threadlists[threadid].push_back(act);
266 void SCAnalysis::reset(action_list_t *list) {
267 for (int t = 0; t <= maxthreads; t++) {
268 action_list_t *tlt = &threadlists[t];
271 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
272 ModelAction *act = *it;
273 delete cvmap.get(act);
274 cvmap.put(act, NULL);
280 bool SCAnalysis::updateConstraints(ModelAction *act) {
281 bool changed = false;
282 for (int i = 0; i <= maxthreads; i++) {
283 thread_id_t tid = int_to_id(i);
284 if (tid == act->get_tid())
287 action_list_t *list = &threadlists[id_to_int(tid)];
288 for (action_list_t::iterator rit = list->begin(); rit != list->end(); rit++) {
289 ModelAction *write = *rit;
290 if (!write->is_write())
292 ClockVector *writecv = cvmap.get(write);
293 if (writecv->synchronized_since(act))
295 if (write->get_location() == act->get_location()) {
296 //write is sc after act
297 merge(writecv, write, act);
306 bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) {
307 bool changed = false;
309 /* Merge in the clock vector from the write */
310 const ModelAction *write = read->get_reads_from();
311 ClockVector *writecv = cvmap.get(write);
312 changed |= merge(cv, read, write) && (*read < *write);
314 for (int i = 0; i <= maxthreads; i++) {
315 thread_id_t tid = int_to_id(i);
316 if (tid == read->get_tid())
318 if (tid == write->get_tid())
320 action_list_t *list = execution->get_actions_on_obj(read->get_location(), tid);
323 for (action_list_t::reverse_iterator rit = list->rbegin(); rit != list->rend(); rit++) {
324 ModelAction *write2 = *rit;
325 if (!write2->is_write())
328 ClockVector *write2cv = cvmap.get(write2);
329 if (write2cv == NULL)
332 /* write -sc-> write2 &&
335 if (write2cv->synchronized_since(write)) {
336 changed |= merge(write2cv, write2, read);
339 //looking for earliest write2 in iteration to satisfy this
342 write2 -sc-> write */
343 if (cv->synchronized_since(write2)) {
344 changed |= writecv == NULL || merge(writecv, write, write2);
352 void SCAnalysis::computeCV(action_list_t *list) {
354 bool firsttime = true;
355 ModelAction **last_act = (ModelAction **)model_calloc(1, (maxthreads + 1) * sizeof(ModelAction *));
357 changed = changed&firsttime;
360 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
361 ModelAction *act = *it;
362 ModelAction *lastact = last_act[id_to_int(act->get_tid())];
363 if (act->is_thread_start())
364 lastact = execution->get_thread(act)->get_creation();
365 last_act[id_to_int(act->get_tid())] = act;
366 ClockVector *cv = cvmap.get(act);
368 cv = new ClockVector(NULL, act);
371 if (lastact != NULL) {
372 merge(cv, act, lastact);
374 if (act->is_thread_join()) {
375 Thread *joinedthr = act->get_thread_operand();
376 ModelAction *finish = execution->get_last_action(joinedthr->get_id());
377 changed |= merge(cv, act, finish);
379 if (act->is_read()) {
380 changed |= processRead(act, cv);
383 /* Reset the last action array */
385 bzero(last_act, (maxthreads + 1) * sizeof(ModelAction *));
388 model_free(last_act);