# Only the python scripts are embeeded in the archive, and the C test files are generated at config time using these scripts.
# These python scripts are copied over from the MBI repository with as little changes as possible.
-set(generator_scripts
+set(generator_scripts
CollArgGenerator.py
CollComGenerator.py
CollLocalConcurrencyGenerator.py
# The following tests are known to fail because simgrid does not intercept local modifications yet
# An idea could be to use ASan on the verified application, along with https://github.com/google/sanitizers/wiki/AddressSanitizerManualPoisoning
- # But currently, ASan is not usable at all, since the Checker dislikes this trick when it tries to read the memory of the app.
+ # But currently, ASan is not usable at all, since the Checker dislikes this trick when it tries to read the memory of the app.
# We should change the checker to not read the app when verifying safty properties
- foreach(localmodif
+ foreach(localmodif
LocalConcurrency_Iallgather_nok LocalConcurrency_Iallgatherv_nok LocalConcurrency_Iallreduce_nok LocalConcurrency_Ialltoall_nok
LocalConcurrency_Ialltoallv_nok LocalConcurrency_Ibcast_nok LocalConcurrency_Iexscan_nok LocalConcurrency_Igather_nok
LocalConcurrency_Irecv_Isend_nok LocalConcurrency_Irecv_Send_init_nok LocalConcurrency_Irecv_Send_nok LocalConcurrency_Ireduce_nok
LocalConcurrency_Iscan_nok LocalConcurrency_Iscatter_nok LocalConcurrency_Recv_Isend_nok LocalConcurrency_Recv_Send_init_nok
LocalConcurrency_Recv_init_Isend_nok LocalConcurrency_Recv_init_Send_nok LocalConcurrency_Recv_init_Send_init_nok
- GlobalConcurrency_Get_Isend_Irecv_nok GlobalConcurrency_Get_Isend_Recv_nok GlobalConcurrency_Get_Send_Irecv_nok GlobalConcurrency_Get_Send_Recv_nok
- GlobalConcurrency_Put_Isend_Irecv_nok GlobalConcurrency_Put_Isend_Recv_nok GlobalConcurrency_Put_Send_Irecv_nok GlobalConcurrency_Put_Send_Recv_nok
+ GlobalConcurrency_Get_Isend_Irecv_nok GlobalConcurrency_Get_Isend_Recv_nok GlobalConcurrency_Get_Send_Irecv_nok GlobalConcurrency_Get_Send_Recv_nok
+ GlobalConcurrency_Put_Isend_Irecv_nok GlobalConcurrency_Put_Isend_Recv_nok GlobalConcurrency_Put_Send_Irecv_nok GlobalConcurrency_Put_Send_Recv_nok
- GlobalConcurrency_rl_Win_fence_Get_rload_nok GlobalConcurrency_rl_Win_fence_Get_rstore_nok
+ GlobalConcurrency_rl_Win_fence_Get_rload_nok GlobalConcurrency_rl_Win_fence_Get_rstore_nok
GlobalConcurrency_rl_Win_fence_Put_rload_nok GlobalConcurrency_rl_Win_fence_Put_rstore_nok
GlobalConcurrency_rl_Win_lock_all_Get_rload_nok GlobalConcurrency_rl_Win_lock_all_Get_rstore_nok
GlobalConcurrency_rl_Win_lock_all_Put_rload_nok GlobalConcurrency_rl_Win_lock_all_Put_rstore_nok
##################################
for c in coll + icoll:
- if c != 'MPI_Barrier': # Barrier has no Data to mismatch or to nullify
- patterns = {}
- patterns = {'c': c}
- patterns['generatedby'] = f'DO NOT EDIT: this file was generated by {os.path.basename(sys.argv[0])}. DO NOT EDIT.'
- patterns['collfeature'] = 'Yes' if c in coll else 'Lacking'
- patterns['icollfeature'] = 'Yes' if c in icoll + ibarrier else 'Lacking'
- patterns['toolfeature'] = 'Lacking'
- patterns['c'] = c
- patterns['init'] = init[c]("1")
- patterns['start'] = start[c]("1")
- patterns['fini'] = fini[c]("1")
- patterns['operation'] = operation[c]("1")
- patterns['free'] = free[c]("1")
- patterns['change_arg'] = ''
-
- # Generate the incorrect matching (datatype Mmismatch)
- replace = patterns
- replace['shortdesc'] = 'Collective @{c}@ with a datatype mismatch'
- replace['longdesc'] = f'Odd ranks use MPI_INT as the datatype while even ranks use MPI_FLOAT'
- replace['outcome'] = 'ERROR: DatatypeMatching'
- replace['errormsg'] = 'Collective datatype mistmatch. @{c}@ at @{filename}@:@{line:MBIERROR2}@ has MPI_INT or MPI_FLOAT as a datatype.'
- replace['change_arg'] = 'if (rank % 2)\n type = MPI_FLOAT; /* MBIERROR1 */'
- make_file(template, f'ParamMatching_Data_{c}_nok.c', replace)
-
- # Generate the call with null type (invalid datatype)
- replace = patterns
- replace['shortdesc'] = 'Collective @{c}@ with an invalid datatype '
- replace['longdesc'] = 'Collective @{c}@ with an invalid datatype '
- replace['outcome'] = 'ERROR: InvalidDatatype'
- replace['errormsg'] = 'Invalid Datatype. @{c}@ at @{filename}@:@{line:MBIERROR2}@ has an invalid datatype.'
- replace['change_arg'] = 'type=MPI_DATATYPE_NULL; /* MBIERROR1 */'
- make_file(template, f'InvalidParam_DataNull_{c}_nok.c', replace)
+ if c != 'MPI_Barrier': # Barrier has no Data to mismatch or to nullify
+ patterns = {}
+ patterns = {'c': c}
+ patterns['generatedby'] = f'DO NOT EDIT: this file was generated by {os.path.basename(sys.argv[0])}. DO NOT EDIT.'
+ patterns['collfeature'] = 'Yes' if c in coll else 'Lacking'
+ patterns['icollfeature'] = 'Yes' if c in icoll + ibarrier else 'Lacking'
+ patterns['toolfeature'] = 'Lacking'
+ patterns['c'] = c
+ patterns['init'] = init[c]("1")
+ patterns['start'] = start[c]("1")
+ patterns['fini'] = fini[c]("1")
+ patterns['operation'] = operation[c]("1")
+ patterns['free'] = free[c]("1")
+ patterns['change_arg'] = ''
+
+ # Generate the incorrect matching (datatype Mmismatch)
+ replace = patterns
+ replace['shortdesc'] = 'Collective @{c}@ with a datatype mismatch'
+ replace['longdesc'] = f'Odd ranks use MPI_INT as the datatype while even ranks use MPI_FLOAT'
+ replace['outcome'] = 'ERROR: DatatypeMatching'
+ replace['errormsg'] = 'Collective datatype mistmatch. @{c}@ at @{filename}@:@{line:MBIERROR2}@ has MPI_INT or MPI_FLOAT as a datatype.'
+ replace['change_arg'] = 'if (rank % 2)\n type = MPI_FLOAT; /* MBIERROR1 */'
+ make_file(template, f'ParamMatching_Data_{c}_nok.c', replace)
+
+ # Generate the call with null type (invalid datatype)
+ replace = patterns
+ replace['shortdesc'] = 'Collective @{c}@ with an invalid datatype '
+ replace['longdesc'] = 'Collective @{c}@ with an invalid datatype '
+ replace['outcome'] = 'ERROR: InvalidDatatype'
+ replace['errormsg'] = 'Invalid Datatype. @{c}@ at @{filename}@:@{line:MBIERROR2}@ has an invalid datatype.'
+ replace['change_arg'] = 'type=MPI_DATATYPE_NULL; /* MBIERROR1 */'
+ make_file(template, f'InvalidParam_DataNull_{c}_nok.c', replace)
##################################
# replace['fini1'] = fini[r]("2")
# replace['fini2'] = fini[s]("1")
# make_file(template, f'CollP2PBuffering_{r}_{s}_{c}_nok.c', replace)
-
def build(self, rootdir, cached=True):
"""Rebuilds the tool binaries. By default, we try to reuse the existing build."""
- print ("Nothing to do to rebuild the tool binaries.")
+ print("Nothing to do to rebuild the tool binaries.")
def setup(self, rootdir):
"""
'EBufferingHazard':'Buffering hazard',
'FOK':"Correct execution",
- 'aislinn':'Aislinn','civl':'CIVL','hermes':'Hermes', 'isp':'ISP','itac':'ITAC', 'simgrid':'Mc SimGrid', 'smpi':'SMPI','smpivg':'SMPI+VG', 'mpisv':'MPI-SV', 'must':'MUST', 'parcoach':'PARCOACH'
+ 'aislinn':'Aislinn', 'civl':'CIVL', 'hermes':'Hermes', 'isp':'ISP', 'itac':'ITAC', 'simgrid':'Mc SimGrid', 'smpi':'SMPI', 'smpivg':'SMPI+VG', 'mpisv':'MPI-SV', 'must':'MUST', 'parcoach':'PARCOACH'
}
def parse_one_code(filename):
diagnostic = f'failed to detect an error'
else:
res_category = 'TRUE_POS'
- diagnostic = f'correctly detected an error'
+ diagnostic = f'correctly detected an error'
else:
raise ValueError(f"Unexpected expectation: {expected} (must be OK or ERROR)")
"""
if os.path.exists(f'{cachefile}.txt') and os.path.exists(f'{cachefile}.elapsed') and os.path.exists(f'{cachefile}.md5sum'):
hash_md5 = hashlib.md5()
- with open(filename, 'rb') as sourcefile :
+ with open(filename, 'rb') as sourcefile:
for chunk in iter(lambda: sourcefile.read(4096), b""):
hash_md5.update(chunk)
newdigest = hash_md5.hexdigest()
outfile.write(output)
with open(f'{cachefile}.md5sum', 'w') as outfile:
hashed = hashlib.md5()
- with open(filename, 'rb') as sourcefile :
+ with open(filename, 'rb') as sourcefile:
for chunk in iter(lambda: sourcefile.read(4096), b""):
hashed.update(chunk)
outfile.write(hashed.hexdigest())
replace['longdesc'] = 'Missing Wait. @{s}@ at @{filename}@:@{line:MBIERROR}@ has no completion.'
replace['outcome'] = 'ERROR: MissingWait'
replace['errormsg'] = 'ERROR: MissingWait'
- replace['fini1'] = ' /* MBIERROR MISSING: ' + wait + ' */'
+ replace['fini1'] = ' /* MBIERROR MISSING: ' + wait + ' */'
make_file(template, f'ReqLifecycle_MissingWait_{s}_{r}_nok.c', replace)
if s in psend:
replace['change_com1'] = 'newcom = MPI_COMM_NULL;'
replace['change_com2'] = ""
make_file(template, f'InvalidParam_ComNull_{p1}_{p2}nok.c', replace)
-
replace['outcome'] = 'ERROR: MessageRace'
replace['errormsg'] = 'P2P message race which can cause a deadlock. @{r}@ at @{filename}@:@{line:MBIERROR}@ is called with ANY_SRC.'
make_file(template, f'MessageRace_{r}_{s}_nok.c', replace)
-
replace['longdesc'] = 'Point to point @{r}@ is never executed. Process 1 calls MPI_Finalize and causes a deadlock.'
replace['outcome'] = 'ERROR: CallMatching'
replace['errormsg'] = 'P2P mistmatch. @{r}@ at @{filename}@:@{line:MBIERROR2}@ is never called because of the conditional (@{change_cond}@).'
- replace['operation1'] = operation[s]("1")
+ replace['operation1'] = operation[s]("1")
replace['operation2'] = operation[r]("2")
make_file(template, f'CallOrdering_{r}_{s}_nok.c', replace)
-
replace['change_arg'] = 'MPI_Type_contiguous (2, MPI_INT, &type); MPI_Type_commit(&type);MPI_Type_free(&type); /* MBIERROR2 */'
replace['errormsg'] = 'Invalid Datatype in @{p}@ at @{filename}@:@{line:MBIERROR}@'
make_file(template, f'InvalidParam_DatatypeCond_{e}_{p}_nok.c', replace)
-
make_file(template, f'LocalConcurrency_lloutwindow_{e}_{p1}_{p2}_nok.c', replace)
# Generate a correct code by switching operation1 and operation2
if p2 in store + load + loadstore:
- replace = patterns
- replace['shortdesc'] = 'Correct code using RMA operations'
- replace['longdesc'] = 'Correct code using RMA operations'
- replace['outcome'] = 'OK'
- replace['errormsg'] = 'OK'
- replace['operation1'] = operation[p2]("1")
- replace['operation2'] = operation[p1]("1")
- make_file(template, f'LocalConcurrency_lloutwindow_{e}_{p2}_{p1}_ok.c', replace)
+ replace = patterns
+ replace['shortdesc'] = 'Correct code using RMA operations'
+ replace['longdesc'] = 'Correct code using RMA operations'
+ replace['outcome'] = 'OK'
+ replace['errormsg'] = 'OK'
+ replace['operation1'] = operation[p2]("1")
+ replace['operation2'] = operation[p1]("1")
+ make_file(template, f'LocalConcurrency_lloutwindow_{e}_{p2}_{p1}_ok.c', replace)
# Generate a correct code by removing operation2
replace = patterns
replace['shortdesc'] = 'Correct code using RMA operations'
for p in put + get:
for s in send + isend:
- for r in recv + irecv:
- patterns = {}
- patterns = {'p': p, 's': s, 'r': r}
- patterns['generatedby'] = f'DO NOT EDIT: this file was generated by {os.path.basename(sys.argv[0])}. DO NOT EDIT.'
- patterns['rmafeature'] = 'Yes'
- patterns['p2pfeature'] = 'Yes' if s in send or r in recv else 'Lacking'
- patterns['ip2pfeature'] = 'Yes' if s in isend or r in irecv else 'Lacking'
- patterns['p'] = p
- patterns['s'] = s
- patterns['r'] = r
- patterns['init1'] = init[p]("1")
- patterns['init2'] = init[s]("2")
- patterns['init3'] = init[r]("3")
- patterns['fini2'] = fini[s]("2")
- patterns['fini3'] = fini[r]("3")
- patterns['operation1'] = operation[p]("1") #put or get
- patterns['operation2'] = operation[s]("2") #send
- patterns['operation3'] = operation[r]("3") #recv
-
- replace = patterns
- replace['shortdesc'] = 'Global Concurrency error.'
- replace['longdesc'] = 'Global Concurrency error. Concurrent access of variable winbuf by @{p}@ and @{r}@'
- replace['outcome'] = 'ERROR: GlobalConcurrency'
- replace['errormsg'] = 'Global Concurrency error. @{p}@ at @{filename}@:@{line:MBIERROR1}@ accesses the window of process 1. Process 1 receives data from process 2 and uses variable winbuf. winbuf in process 1 is then nondeterministic.'
- make_file(template, f'GlobalConcurrency_{p}_{s}_{r}_nok.c', replace)
+ for r in recv + irecv:
+ patterns = {}
+ patterns = {'p': p, 's': s, 'r': r}
+ patterns['generatedby'] = f'DO NOT EDIT: this file was generated by {os.path.basename(sys.argv[0])}. DO NOT EDIT.'
+ patterns['rmafeature'] = 'Yes'
+ patterns['p2pfeature'] = 'Yes' if s in send or r in recv else 'Lacking'
+ patterns['ip2pfeature'] = 'Yes' if s in isend or r in irecv else 'Lacking'
+ patterns['p'] = p
+ patterns['s'] = s
+ patterns['r'] = r
+ patterns['init1'] = init[p]("1")
+ patterns['init2'] = init[s]("2")
+ patterns['init3'] = init[r]("3")
+ patterns['fini2'] = fini[s]("2")
+ patterns['fini3'] = fini[r]("3")
+ patterns['operation1'] = operation[p]("1") #put or get
+ patterns['operation2'] = operation[s]("2") #send
+ patterns['operation3'] = operation[r]("3") #recv
+
+ replace = patterns
+ replace['shortdesc'] = 'Global Concurrency error.'
+ replace['longdesc'] = 'Global Concurrency error. Concurrent access of variable winbuf by @{p}@ and @{r}@'
+ replace['outcome'] = 'ERROR: GlobalConcurrency'
+ replace['errormsg'] = 'Global Concurrency error. @{p}@ at @{filename}@:@{line:MBIERROR1}@ accesses the window of process 1. Process 1 receives data from process 2 and uses variable winbuf. winbuf in process 1 is then nondeterministic.'
+ make_file(template, f'GlobalConcurrency_{p}_{s}_{r}_nok.c', replace)
for e in epoch:
for p1 in get:
- for p2 in put + rstore + rload + get :
+ for p2 in put + rstore + rload + get:
patterns = {}
patterns = {'e': e, 'p1': p1, 'p2': p2}
patterns['generatedby'] = f'DO NOT EDIT: this file was generated by {os.path.basename(sys.argv[0])}. DO NOT EDIT.'
# Replace Put first argument
if p2 in put:
- replace['operation2'] = 'MPI_Put(&winbuf[20], N, MPI_INT, target, 0, N, type, win);'
+ replace['operation2'] = 'MPI_Put(&winbuf[20], N, MPI_INT, target, 0, N, type, win);'
make_file(template, f'GlobalConcurrency_rl_{e}_{p1}_{p2}_nok.c', replace)
replace['outcome'] = 'ERROR: GlobalConcurrency'
replace['errormsg'] = 'Global Concurrency error. @{p1}@ at @{filename}@:@{line:MBIERROR1}@ conflicts in process 1'
make_file(template, f'GlobalConcurrency_rr_{e}_{p1}_nok.c', replace)
-
"""
-for b in ['missing', 'null', 'malloc', 'bufferSize']:
+for b in ['missing', 'null', 'malloc', 'bufferSize']:
patterns = {}
patterns = {'b': b}
patterns['origin'] = "MPI-CorrBench"
import re
# Collectives
-coll = ['MPI_Barrier','MPI_Bcast', 'MPI_Reduce', 'MPI_Gather', 'MPI_Scatter', 'MPI_Scan', 'MPI_Exscan', 'MPI_Allgather', 'MPI_Allreduce', 'MPI_Allgatherv', 'MPI_Alltoall', 'MPI_Alltoallv']
+coll = ['MPI_Barrier', 'MPI_Bcast', 'MPI_Reduce', 'MPI_Gather', 'MPI_Scatter', 'MPI_Scan', 'MPI_Exscan', 'MPI_Allgather', 'MPI_Allreduce', 'MPI_Allgatherv', 'MPI_Alltoall', 'MPI_Alltoallv']
icoll = ['MPI_Ibcast', 'MPI_Ireduce', 'MPI_Igather', 'MPI_Iscatter', 'MPI_Iscan', 'MPI_Iexscan', 'MPI_Iallgather', 'MPI_Iallreduce', 'MPI_Iallgatherv', 'MPI_Ialltoall', 'MPI_Ialltoallv']
ibarrier = ['MPI_Ibarrier']
coll4op = ['MPI_Reduce', 'MPI_Allreduce']
icoll4op = ['MPI_Ireduce', 'MPI_Iallreduce']
-coll4root = ['MPI_Reduce', 'MPI_Bcast', 'MPI_Gather', 'MPI_Scatter']
+coll4root = ['MPI_Reduce', 'MPI_Bcast', 'MPI_Gather', 'MPI_Scatter']
icoll4root = ['MPI_Ireduce', 'MPI_Ibcast', 'MPI_Igather', 'MPI_Iscatter']
pcoll = []
tcoll = ['MPI_Comm_split', 'MPI_Op_create', 'MPI_Comm_dup', 'MPI_Type_contiguous', 'MPI_Comm_create', 'MPI_Group_excl'] # MPI_Comm_dup removed
tcoll4topo = ['MPI_Cart_get']
# P2P
-allsend = ['MPI_Send', 'MPI_Isend', 'MPI_Ssend', 'MPI_Bsend','MPI_Send_init']
+allsend = ['MPI_Send', 'MPI_Isend', 'MPI_Ssend', 'MPI_Bsend', 'MPI_Send_init']
allrecv = ['MPI_Recv', 'MPI_Irecv', 'MPI_Recv_init']
send = ['MPI_Send']
ssend = ['MPI_Ssend']
### RMA
-epoch['MPI_Win_fence'] =lambda n: 'MPI_Win_fence(0, win);'
-finEpoch['MPI_Win_fence'] =lambda n: 'MPI_Win_fence(0, win);'
-epoch['MPI_Win_lock'] =lambda n: 'MPI_Win_lock(MPI_LOCK_SHARED, target, 0, win);'
-finEpoch['MPI_Win_lock'] =lambda n: 'MPI_Win_unlock(target, win);'
-epoch['MPI_Win_lock_all'] =lambda n: 'MPI_Win_lock_all(0,win);'
-finEpoch['MPI_Win_lock_all'] =lambda n: 'MPI_Win_unlock_all(win);'
+epoch['MPI_Win_fence'] = lambda n: 'MPI_Win_fence(0, win);'
+finEpoch['MPI_Win_fence'] = lambda n: 'MPI_Win_fence(0, win);'
+epoch['MPI_Win_lock'] = lambda n: 'MPI_Win_lock(MPI_LOCK_SHARED, target, 0, win);'
+finEpoch['MPI_Win_lock'] = lambda n: 'MPI_Win_unlock(target, win);'
+epoch['MPI_Win_lock_all'] = lambda n: 'MPI_Win_lock_all(0,win);'
+finEpoch['MPI_Win_lock_all'] = lambda n: 'MPI_Win_unlock_all(win);'
init['MPI_Put'] = lambda n: f'int localbuf{n}[N] = {{12345}};'
operation['MPI_Put'] = lambda n: f'MPI_Put(&localbuf{n}, N, MPI_INT, target, 0, N, type, win);'
if os.path.exists(filename):
with open(filename, 'r') as file:
prev = file.read().split('\n')[0]
- prev = re.sub('^.*?scripts/','scripts/', prev)
+ prev = re.sub('^.*?scripts/', 'scripts/', prev)
prev = re.sub('. DO NOT EDIT.', '', prev)
now = output.split('\n')[0]
- now = re.sub('^.*?scripts/','scripts/', now)
+ now = re.sub('^.*?scripts/', 'scripts/', now)
now = re.sub('. DO NOT EDIT.', '', now)
print(f'WARNING: overwriting {filename}. Previously generated by: {prev}; regenerated by {now}')
if re.search('DFS exploration ended.', output):
return 'OK'
- print (f">>>>[ INCONCLUSIVE ]>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> ({cachefile})")
+ print(f">>>>[ INCONCLUSIVE ]>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> ({cachefile})")
print(output)
- print ("<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<")
+ print("<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<")
return 'other'
