Skip to content

Commit

Permalink
fixed parallel issue
Browse files Browse the repository at this point in the history
  • Loading branch information
Guillermo A. Perez committed May 28, 2015
1 parent 24c25a4 commit 8975232
Show file tree
Hide file tree
Showing 2 changed files with 28 additions and 53 deletions.
8 changes: 0 additions & 8 deletions source/abssynthe.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -169,14 +169,6 @@ int main (int argc, char** argv) {
result = compSolve2(&aig);
} else if (settings.comp_algo == 3){
result = compSolve3(&aig);
#ifndef NDEBUG
dbgMsg("Decomposition took: " +
std::to_string(getAccTime("decompose")/(double)CLOCKS_PER_SEC));
dbgMsg("Local steps took: " +
std::to_string(getAccTime("localstep")/(double)CLOCKS_PER_SEC));
dbgMsg("Global steps took: " +
std::to_string(getAccTime("globalstep")/(double)CLOCKS_PER_SEC));
#endif
} else { // traditional fixpoint computation
result = solve(&aig);
}
Expand Down
73 changes: 28 additions & 45 deletions source/algos.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,6 @@
#include <ctime>
#include <list>
#include <set>
#include <tuple>
#include <cfloat>
#include "cuddObj.hh"

Expand Down Expand Up @@ -210,8 +209,8 @@ static vector<pair<unsigned, BDD>> synthAlgo(Cudd* mgr, BDDAIG* spec,
return result;
}

void finalizeSynth(Cudd* mgr, BDDAIG* spec,
vector<pair<unsigned, BDD>> result) {
static void finalizeSynth(Cudd* mgr, BDDAIG* spec,
vector<pair<unsigned, BDD>> result) {
// let us clean the AIG before we start introducing new stuff
spec->removeErrorLatch();
// we now get rid of all controllable inputs in the aig spec by replacing
Expand Down Expand Up @@ -264,7 +263,7 @@ static BDD upre(BDDAIG* spec, BDD dst, BDD &trans_bdd) {
return temp_bdd.ExistAbstract(uinput_cube);
}

bool internalSolve(Cudd* mgr, BDDAIG* spec, const BDD* upre_init,
static bool internalSolve(Cudd* mgr, BDDAIG* spec, const BDD* upre_init,
BDD* losing_region, BDD* losing_transitions,
bool do_synth=false) {
//static int occ_counter = 1;
Expand Down Expand Up @@ -306,11 +305,8 @@ bool internalSolve(Cudd* mgr, BDDAIG* spec, const BDD* upre_init,
if (!includes_init && do_synth && settings.out_file != NULL) {
dbgMsg("Starting synthesis, acquiring lock on synth mutex");
if (data != NULL) pthread_mutex_lock(&data->synth_mutex);
if (data == NULL || !data->done) {
finalizeSynth(mgr, spec,
synthAlgo(mgr, spec, ~bad_transitions, ~error_states));
}
if (data != NULL) pthread_mutex_unlock(&data->synth_mutex);
finalizeSynth(mgr, spec,
synthAlgo(mgr, spec, ~bad_transitions, ~error_states));
}
return !includes_init;
}
Expand Down Expand Up @@ -393,12 +389,9 @@ bool compSolve1(AIG* spec_base) {
if (!includes_init && settings.out_file != NULL) {
dbgMsg("Starting synthesis, acquiring lock on synth mutex");
if (data != NULL) pthread_mutex_lock(&data->synth_mutex);
if (data == NULL || !data->done) {
finalizeSynth(&mgr, &spec,
synthAlgo(&mgr, &spec, ~bad_transitions,
~error_states));
}
if (data != NULL) pthread_mutex_unlock(&data->synth_mutex);
finalizeSynth(&mgr, &spec,
synthAlgo(&mgr, &spec, ~bad_transitions,
~error_states));
}

} else if (settings.out_file != NULL) {
Expand All @@ -408,22 +401,19 @@ bool compSolve1(AIG* spec_base) {
//std::cout << ("Starting synthesis, acquiring lock on synth mutex\n");
//std::cout.flush();
if (data != NULL) pthread_mutex_lock(&data->synth_mutex);
if (data == NULL || !data->done) {
vector<pair<unsigned, BDD>> all_cinput_strats;
vector<pair<BDD, BDD>>::iterator sg = subgame_results.begin();
logMsg("Doing stuff");
for (vector<BDDAIG*>::iterator i = subgames.begin();
i != subgames.end(); i++) {
vector<pair<unsigned, BDD>> temp;
temp = synthAlgo(&mgr, *i, ~sg->second, ~sg->first);
all_cinput_strats.insert(all_cinput_strats.end(),
temp.begin(), temp.end());
sg++;
delete *i;
}
finalizeSynth(&mgr, &spec, all_cinput_strats);
vector<pair<unsigned, BDD>> all_cinput_strats;
vector<pair<BDD, BDD>>::iterator sg = subgame_results.begin();
logMsg("Doing stuff");
for (vector<BDDAIG*>::iterator i = subgames.begin();
i != subgames.end(); i++) {
vector<pair<unsigned, BDD>> temp;
temp = synthAlgo(&mgr, *i, ~sg->second, ~sg->first);
all_cinput_strats.insert(all_cinput_strats.end(),
temp.begin(), temp.end());
sg++;
delete *i;
}
if (data != NULL) pthread_mutex_unlock(&data->synth_mutex);
finalizeSynth(&mgr, &spec, all_cinput_strats);
}

return !includes_init;
Expand Down Expand Up @@ -521,12 +511,9 @@ bool compSolve2(AIG* spec_base) {
if (settings.out_file != NULL) {
dbgMsg("Starting synthesis, acquiring lock on synth mutex");
if (data != NULL) pthread_mutex_lock(&data->synth_mutex);
if (data == NULL || !data->done) {
finalizeSynth(&mgr, &spec,
synthAlgo(&mgr, &spec, ~subgame_results.back().first,
mgr.bddOne()));
}
if (data != NULL) pthread_mutex_unlock(&data->synth_mutex);
finalizeSynth(&mgr, &spec,
synthAlgo(&mgr, &spec, ~subgame_results.back().first,
mgr.bddOne()));

}
return true;
Expand All @@ -537,7 +524,6 @@ bool compSolve3(AIG* spec_base) {
Cudd mgr(0, 0);
mgr.AutodynEnable(CUDD_REORDER_SIFT);
BDDAIG spec(*spec_base, &mgr);
resetTimer("decompose");
vector<BDDAIG*> subgames = spec.decompose();
if (subgames.size() == 0) return internalSolve(&mgr, &spec, NULL, NULL, NULL,
true);
Expand Down Expand Up @@ -576,7 +562,6 @@ bool compSolve3(AIG* spec_base) {
while (!includes_init && prev_lose != global_lose) {
prev_lose = global_lose;
dbgMsg("Refinement iterate: " + to_string(count++));
resetTimer("localstep");
for (int i = 0; i < subgames.size(); i++) {
BDDAIG* subgame = subgames[i];
subgame_info &sg_info = subgame_results[i];
Expand Down Expand Up @@ -608,7 +593,6 @@ bool compSolve3(AIG* spec_base) {
addTime("localstep");
if (global_lose == prev_lose) {
dbgMsg("Global Upre");
resetTimer("globalstep");
global_lose = global_lose | upre(&spec, global_lose, global_losing_trans);
addTime("globalstep");
} else {
Expand All @@ -626,11 +610,8 @@ bool compSolve3(AIG* spec_base) {
if (!includes_init && settings.out_file != NULL) {
dbgMsg("Starting synthesis, acquiring lock on synth mutex");
if (data != NULL) pthread_mutex_lock(&data->synth_mutex);
if (data == NULL || !data->done) {
finalizeSynth(&mgr, &spec,
synthAlgo(&mgr, &spec, ~global_losing_trans, ~global_lose));
}
if (data != NULL) pthread_mutex_unlock(&data->synth_mutex);
finalizeSynth(&mgr, &spec,
synthAlgo(&mgr, &spec, ~global_losing_trans, ~global_lose));
}

return !includes_init;
Expand Down Expand Up @@ -709,7 +690,9 @@ bool solveParallel() {

// the parent waits for one child to finish
int status;
wait(&status);
pid_t kiddo = wait(&status);
dbgMsg("Answer from process " + to_string(kiddo));
dbgMsg("With status " + to_string(status));
// then the parent kills all its children
for (int i = 0; i < 4; i++)
kill(children[i], SIGKILL);
Expand Down

0 comments on commit 8975232

Please sign in to comment.