- Bugfixed claims.c (r722 log), although the reason for fixing and the
error itself is quite irreproducable.
This commit is contained in:
ccremers
parent
7ce5736af3
commit
1c234e3cee
366
src/claims.c
366
src/claims.c
@ -10,26 +10,46 @@
|
||||
#define LABEL_GOOD -3
|
||||
#define LABEL_TODO -2
|
||||
|
||||
// Debugging the NI-SYNCH checks
|
||||
//#define OKIDEBUG
|
||||
|
||||
/*
|
||||
* Validity checks for claims
|
||||
*/
|
||||
|
||||
#ifdef OKIDEBUG
|
||||
int indac = 0;
|
||||
|
||||
void indact ()
|
||||
{
|
||||
int i;
|
||||
|
||||
i = indac;
|
||||
while (i > 0)
|
||||
{
|
||||
printf ("| ");
|
||||
i--;
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
//! Check complete message match
|
||||
/**
|
||||
*@returns any of the MATCH_ signals
|
||||
*/
|
||||
int
|
||||
__inline__ int
|
||||
events_match (const System sys, const int i, const int j)
|
||||
{
|
||||
Roledef rdi, rdj;
|
||||
|
||||
rdi = sys->traceEvent[i];
|
||||
rdj = sys->traceEvent[j];
|
||||
if ((isTermEqual (rdi->message, rdj->message)) &&
|
||||
(isTermEqual (rdi->from, rdj->from)) &&
|
||||
(isTermEqual (rdi->to, rdj->to)) &&
|
||||
(isTermEqual (rdi->label, rdj->label)) &&
|
||||
!(rdi->internal || rdj->internal))
|
||||
if (isTermEqual (rdi->message, rdj->message) &&
|
||||
isTermEqual (rdi->from, rdj->from) &&
|
||||
isTermEqual (rdi->to, rdj->to) &&
|
||||
isTermEqual (rdi->label, rdj->label) &&
|
||||
!(rdi->internal || rdj->internal)
|
||||
)
|
||||
{
|
||||
if (rdi->type == SEND && rdj->type == READ)
|
||||
{
|
||||
@ -49,131 +69,239 @@ events_match (const System sys, const int i, const int j)
|
||||
return MATCH_NONE;
|
||||
}
|
||||
|
||||
|
||||
//! Check nisynch from label_to_index.
|
||||
__inline__ int
|
||||
oki_nisynch_full (const System sys, const Termmap label_to_index)
|
||||
{
|
||||
// Are all labels well linked?
|
||||
Termmap label_to_index_scan;
|
||||
|
||||
label_to_index_scan = label_to_index;
|
||||
while (label_to_index_scan != NULL)
|
||||
{
|
||||
if (label_to_index_scan->result != LABEL_GOOD)
|
||||
{
|
||||
#ifdef OKIDEBUG
|
||||
indact ();
|
||||
printf ("Incorrectly linked label at the end,");
|
||||
printf ("label: ");
|
||||
termPrint (label_to_index_scan->term);
|
||||
printf ("\n");
|
||||
#endif
|
||||
return 0;
|
||||
}
|
||||
label_to_index_scan = label_to_index_scan->next;
|
||||
}
|
||||
// Apparently they are all well linked
|
||||
return 1;
|
||||
}
|
||||
|
||||
//! Evaluate claims or internal reads (chooses)
|
||||
__inline__ int
|
||||
oki_nisynch_other (const System sys, const int trace_index, const Termmap role_to_run, const Termmap label_to_index)
|
||||
{
|
||||
int result;
|
||||
|
||||
#ifdef OKIDEBUG
|
||||
indact ();
|
||||
printf ("Exploring further assuming this (claim) run is not involved.\n");
|
||||
indac++;
|
||||
#endif
|
||||
result = oki_nisynch (sys, trace_index-1, role_to_run, label_to_index);
|
||||
#ifdef OKIDEBUG
|
||||
indact ();
|
||||
printf (">%i<\n", result);
|
||||
indac--;
|
||||
#endif
|
||||
return result;
|
||||
}
|
||||
|
||||
//! Evaluate reads
|
||||
__inline__ int
|
||||
oki_nisynch_read (const System sys, const int trace_index, const Termmap role_to_run, const Termmap label_to_index)
|
||||
{
|
||||
/*
|
||||
* Read is only relevant for already involved runs, and labels in prec
|
||||
*/
|
||||
Termmap role_to_run_scan;
|
||||
int result = 7;
|
||||
Roledef rd;
|
||||
int rid;
|
||||
|
||||
rd = sys->traceEvent[trace_index];
|
||||
rid = sys->traceRun[trace_index];
|
||||
|
||||
role_to_run_scan = role_to_run;
|
||||
while (role_to_run_scan != NULL)
|
||||
{
|
||||
if (role_to_run_scan->result == rid)
|
||||
{
|
||||
// Involved, but is it a prec label?
|
||||
if (termmapGet (label_to_index, rd->label) == LABEL_TODO)
|
||||
{
|
||||
Termmap label_to_index_buf;
|
||||
int result;
|
||||
|
||||
label_to_index_buf = termmapDuplicate (label_to_index);
|
||||
label_to_index_buf = termmapSet (label_to_index_buf, rd->label, trace_index);
|
||||
#ifdef OKIDEBUG
|
||||
indact ();
|
||||
printf ("Exploring because this (read) run is involved.\n");
|
||||
indac++;
|
||||
#endif
|
||||
result = oki_nisynch (sys, trace_index-1, role_to_run, label_to_index_buf);
|
||||
#ifdef OKIDEBUG
|
||||
indact ();
|
||||
printf (">%i<\n", result);
|
||||
indac--;
|
||||
#endif
|
||||
termmapDelete (label_to_index_buf);
|
||||
return result;
|
||||
}
|
||||
}
|
||||
role_to_run_scan = role_to_run_scan->next;
|
||||
}
|
||||
// Apparently not involved
|
||||
#ifdef OKIDEBUG
|
||||
indact ();
|
||||
printf ("Exploring further assuming this (read) run is not involved.\n");
|
||||
indac++;
|
||||
#endif
|
||||
result = oki_nisynch (sys, trace_index-1, role_to_run, label_to_index);
|
||||
#ifdef OKIDEBUG
|
||||
indac--;
|
||||
#endif
|
||||
return result;
|
||||
}
|
||||
|
||||
|
||||
//! Evaluate sends
|
||||
__inline__ int
|
||||
oki_nisynch_send (const System sys, const int trace_index, const Termmap role_to_run, const Termmap label_to_index)
|
||||
{
|
||||
Roledef rd;
|
||||
int rid;
|
||||
int result = 8;
|
||||
int old_run;
|
||||
Term rolename;
|
||||
|
||||
rd = sys->traceEvent[trace_index];
|
||||
rid = sys->traceRun[trace_index];
|
||||
/*
|
||||
* Two options: it is either involved or not
|
||||
*/
|
||||
// 1. Assume that this run is not yet involved
|
||||
#ifdef OKIDEBUG
|
||||
indact ();
|
||||
printf ("Exploring further assuming (send) run %i is not involved.\n", rid);
|
||||
indac++;
|
||||
#endif
|
||||
result = oki_nisynch (sys, trace_index-1, role_to_run, label_to_index);
|
||||
#ifdef OKIDEBUG
|
||||
indact ();
|
||||
printf (">%i<\n", result);
|
||||
indac--;
|
||||
#endif
|
||||
if (result)
|
||||
return 1;
|
||||
|
||||
#ifdef OKIDEBUG
|
||||
indact ();
|
||||
printf ("Exploring when %i is involved.\n", rid);
|
||||
#endif
|
||||
// 2. It is involved. Then either already used for this role, or will be now.
|
||||
rolename = sys->runs[rid].role->nameterm;
|
||||
old_run = termmapGet (role_to_run, rolename); // what was already stored for this role as the runid
|
||||
if (old_run == -1 || old_run == rid)
|
||||
{
|
||||
int partner_index;
|
||||
|
||||
// Was not involved yet in a registerd way, or was the correct rid
|
||||
partner_index = termmapGet (label_to_index, rd->label);
|
||||
// Ordered match needed for this label
|
||||
// So it already needs to be filled by a read
|
||||
if (partner_index >= 0)
|
||||
{
|
||||
// There is already a read for it
|
||||
if (events_match (sys, partner_index, trace_index) == MATCH_ORDER)
|
||||
{
|
||||
// They match in the right order
|
||||
Termmap role_to_run_buf, label_to_index_buf;
|
||||
|
||||
#ifdef OKIDEBUG
|
||||
indact ();
|
||||
printf ("Matching messages found for label ");
|
||||
termPrint (rd->label);
|
||||
printf ("\n");
|
||||
#endif
|
||||
/**
|
||||
*@todo Optimization can be done when old_run == rid, no copy of role_to_run needs to be made.
|
||||
*/
|
||||
role_to_run_buf = termmapDuplicate (role_to_run);
|
||||
role_to_run_buf = termmapSet (role_to_run_buf, rolename, rid);
|
||||
label_to_index_buf = termmapDuplicate (label_to_index);
|
||||
label_to_index_buf = termmapSet (label_to_index_buf, rd->label, LABEL_GOOD);
|
||||
#ifdef OKIDEBUG
|
||||
indact ();
|
||||
printf ("In NI-Synch scan, assuming %i run is involved.\n", rid);
|
||||
indact ();
|
||||
printf ("Exploring further assuming this matching, which worked.\n");
|
||||
indac++;
|
||||
#endif
|
||||
result = oki_nisynch (sys, trace_index-1, role_to_run_buf, label_to_index_buf);
|
||||
#ifdef OKIDEBUG
|
||||
indact ();
|
||||
printf (">%i<\n", result);
|
||||
indac--;
|
||||
#endif
|
||||
termmapDelete (label_to_index_buf);
|
||||
termmapDelete (role_to_run_buf);
|
||||
return result;
|
||||
}
|
||||
}
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
||||
|
||||
//! nisynch generalization
|
||||
/**
|
||||
* f maps the involved roles to run identifiers.
|
||||
* g maps all labels in prec to the event indices for things already found,
|
||||
* role_to_run maps the involved roles to run identifiers.
|
||||
* label_to_index maps all labels in prec to the event indices for things already found,
|
||||
* or to LABEL_TODO for things not found yet but in prec, and LABEL_GOOD for well linked messages (and that have thus defined a runid for the corresponding role).
|
||||
* All values not in prec map to -1.
|
||||
*@returns 1 iff the claim is allright, 0 iff it is violated.
|
||||
*/
|
||||
int
|
||||
oki_nisynch (const System sys, const int i, const Termmap f, const Termmap g)
|
||||
oki_nisynch (const System sys, const int trace_index, const Termmap role_to_run, const Termmap label_to_index)
|
||||
{
|
||||
int type;
|
||||
|
||||
// Check for completed trace
|
||||
if (i < 0)
|
||||
{
|
||||
// Are all labels well linked?
|
||||
Termmap gscan;
|
||||
if (trace_index < 0)
|
||||
return oki_nisynch_full (sys, label_to_index);
|
||||
|
||||
gscan = g;
|
||||
while (gscan != NULL)
|
||||
{
|
||||
if (gscan->result != LABEL_GOOD)
|
||||
return 0;
|
||||
gscan = gscan->next;
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
Roledef rd;
|
||||
int rid;
|
||||
#ifdef OKIDEBUG
|
||||
indact ();
|
||||
printf ("Checking event %i", trace_index);
|
||||
printf (" = #%i : ", sys->traceRun[trace_index]);
|
||||
roledefPrint (sys->traceEvent[trace_index]);
|
||||
printf ("\n");
|
||||
#endif
|
||||
|
||||
rd = sys->traceEvent[i];
|
||||
rid = sys->traceRun[i];
|
||||
/*
|
||||
* Simple case: internal event or claim
|
||||
*/
|
||||
if (rd->type == CLAIM || rd->internal)
|
||||
{
|
||||
return oki_nisynch (sys,i-1,f,g);
|
||||
}
|
||||
else
|
||||
{
|
||||
/*
|
||||
* More difficult cases: send and read
|
||||
*/
|
||||
if (rd->type == READ)
|
||||
{
|
||||
/*
|
||||
* Read is only relevant for already involved runs, and labels in prec
|
||||
*/
|
||||
Termmap fscan;
|
||||
type = sys->traceEvent[trace_index]->type;
|
||||
|
||||
fscan = f;
|
||||
while (fscan != NULL)
|
||||
{
|
||||
if (fscan->result == rid)
|
||||
{
|
||||
// Involved, but is it a prec label?
|
||||
if (termmapGet (g, rd->label) == LABEL_TODO)
|
||||
{
|
||||
Termmap gbuf;
|
||||
int result;
|
||||
|
||||
gbuf = termmapDuplicate (g);
|
||||
gbuf = termmapSet (gbuf, rd->label, i);
|
||||
result = oki_nisynch (sys,i-1,f,gbuf);
|
||||
termmapDelete (gbuf);
|
||||
return result;
|
||||
}
|
||||
}
|
||||
fscan = fscan->next;
|
||||
}
|
||||
// Apparently not involved
|
||||
return oki_nisynch (sys,i-1,f,g);
|
||||
}
|
||||
if (rd->type == SEND)
|
||||
{
|
||||
// Scan whether we were waiting for it or not
|
||||
int result;
|
||||
int rid2;
|
||||
Term rolename;
|
||||
|
||||
/*
|
||||
* Two options: it is either involved or not
|
||||
*/
|
||||
// 1. Assume that this run is not yet involved
|
||||
result = oki_nisynch (sys, i-1, f, g);
|
||||
// 2. It is involved. Then either already used for this role, or will be now.
|
||||
rolename = sys->runs[rid].role->nameterm;
|
||||
rid2 = termmapGet (f, rolename);
|
||||
if (rid2 == -1 || rid2 == rid)
|
||||
{
|
||||
Termmap gscan;
|
||||
// Was not involved yet in a registerd way, or was the correct rid
|
||||
gscan = g;
|
||||
while (!result && gscan != NULL)
|
||||
{
|
||||
// Ordered match needed
|
||||
if (gscan->result > -1 &&
|
||||
events_match (sys, gscan->result, i) == 1)
|
||||
{
|
||||
Termmap fbuf, gbuf;
|
||||
|
||||
/**
|
||||
*@todo Optimization can be done when rid2 == rid, no copy of f needs to be made.
|
||||
*/
|
||||
fbuf = termmapDuplicate (f);
|
||||
fbuf = termmapSet (fbuf, rolename, rid);
|
||||
gbuf = termmapDuplicate (g);
|
||||
gbuf = termmapSet (gbuf, rd->label, -3);
|
||||
result = oki_nisynch (sys, i-1, fbuf, gbuf);
|
||||
termmapDelete (gbuf);
|
||||
termmapDelete (fbuf);
|
||||
}
|
||||
gscan = gscan->next;
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
/*
|
||||
* Exception: no send, no read, what is it?
|
||||
*/
|
||||
error ("Unrecognized event type in claim scanner at %i.", i);
|
||||
}
|
||||
}
|
||||
if (type == CLAIM || sys->traceEvent[trace_index]->internal)
|
||||
return oki_nisynch_other (sys, trace_index, role_to_run, label_to_index);
|
||||
if (type == READ)
|
||||
return oki_nisynch_read (sys, trace_index, role_to_run, label_to_index);
|
||||
if (type == SEND)
|
||||
return oki_nisynch_send (sys, trace_index, role_to_run, label_to_index);
|
||||
/*
|
||||
* Exception: no claim, no send, no read, what is it?
|
||||
*/
|
||||
error ("Unrecognized event type in claim scanner at %i.", trace_index);
|
||||
}
|
||||
|
||||
/*
|
||||
|
||||
Loading…
Reference in New Issue
Block a user