/*
configuration to inspect the histogram:
const int B = 1; // number of computations in a batch
const int K = 1; // maximum difference of batches among processors
const int N = 1; // number of computing cores
*/
const int N = 1; // number of processors
const int B = 1; // number of runs in a batch
const int K = 1; // maximum difference of batches among processors
/*
const int B_vals[10] = {1,2,3,4,5,6,7,8,9,10};
const int B = B_vals[#range(0, 9, B)];
const int N_vals[6] = {1, 2, 4, 8, 16, 32};
const int N = N_vals[#range(0, 5, N)];
const int K_vals[4] = {1,2,4,8};
const int K = K_vals[#range(0, 3, K)];
*/
typedef int[0, N-1] node_t;
/*
histogram was acquired from a frequency histogram of the train-gate-stat model using:
property: Pr[ #<= 1000]([] time<= 1000 && forall (i : id_t) forall (j : id_t) Train(i).Cross && Train(j).Cross imply i == j)
with alpha=0.01, epsilon=0.005, bucket-width=1.0
*/
const int H = 58; // number of buckets in a histogram
const int H_offset = 333;
const int H_step = 1;
typedef int[0,H] bucket_t;
const int w[bucket_t] = {
4,1,1,11,8,24,25,60,74,102,194,167,425,436,712,1057,817,2055,1430,2744,2961,2801,
5103,3033,6338,4708,5487,7261,3994,8120,4195,6259,5793,3618,5997,2415,4241,2737,
2042,2620,892,1668,707,758,662,237,400,133,185,101,35,65,10,21,6,6,5,1,5
};
broadcast chan req;
broadcast chan done[node_t];
int batches[node_t], minimum=0;
bool allowedToProceed(const node_t n)
{
return (batches[n] < minimum+K);
}
bool busy[node_t];
clock usage, time;Slaveconst node_t idint counter=0, j;
clock x;
iteratecomputestartMasternode_t id;
void saveWork(const node_t n)
{
if (minimum==batches[n]) {
minimum = ++batches[n];
for (i: node_t)
if (batches[i] < minimum) minimum = batches[i];
if (batches[n]==minimum) { // minimum has been lifted
for (i: node_t) batches[i] -= minimum; // shift all batches
minimum = 0; // reset minimum
}
} else {
batches[n]++;
}
}
DoneGlobal
system Slave, Master, Global;