Implement LP-based OMIP blocking analysis

2 files changed, 302 insertions, 0 deletions

diff --git a/native/src/blocking/linprog/lp_common.cpp b/native/src/blocking/linprog/lp_common.cpp
index 1715d3b..2df1284 100644
--- a/native/src/blocking/linprog/lp_common.cpp
+++ b/native/src/blocking/linprog/lp_common.cpp
@@ -119,6 +119,40 @@ void set_blocking_objective_part_shm(
         }
 }
 
+// This version is for suspension-oblivious shared-memory protocols,
+// where the analysis does not differentiate among the different kinds
+// of blocking (since they are all just added to the execution time anyway).
+void set_blocking_objective_sob(
+        VarMapper& vars,
+        const ResourceSharingInfo& info,
+        const TaskInfo& ti,
+        LinearProgram& lp)
+{
+        LinearExpression *obj;
+
+        obj = lp.get_objective();
+
+        foreach_task_except(info.get_tasks(), ti, tx)
+        {
+                unsigned int t = tx->get_id();
+
+                foreach(tx->get_requests(), request)
+                {
+                        unsigned int q = request->get_resource_id();
+                        double length = request->get_request_length();;
+
+                        foreach_request_instance(*request, ti, v)
+                        {
+                                unsigned int var_id;
+
+                                var_id = vars.lookup(t, q, v, BLOCKING_SOB);
+                                obj->add_term(length, var_id);
+                        }
+                }
+        }
+}
+
+
 // Constraint 1 in [Brandenburg 2013]
 void add_mutex_constraints(
         VarMapper& vars,
diff --git a/native/src/blocking/linprog/lp_omip.cpp b/native/src/blocking/linprog/lp_omip.cpp
new file mode 100644
index 0000000..0e5d864
--- /dev/null
+++ b/native/src/blocking/linprog/lp_omip.cpp
@@ -0,0 +1,268 @@
+#include <iostream>
+#include <set>
+#include <algorithm>
+#include <cmath>
+
+#include "lp_common.h"
+#include "blocking.h"
+#include "stl-hashmap.h"
+
+#include "cpu_time.h"
+
+// Per-cluster, per-resource access counts.
+typedef hashmap<unsigned int, unsigned int> AccessCounts;
+typedef hashmap<unsigned int, AccessCounts> PerClusterACounts;
+
+static AccessCounts count_accesses(
+        const ResourceSharingInfo& info,
+        unsigned int cluster)
+{
+        AccessCounts acount;
+
+        foreach(info.get_tasks(), tx) {
+                if (tx->get_cluster() == cluster) {
+                        foreach(tx->get_requests(), request)
+                        {
+                                unsigned int q = request->get_resource_id();
+                                // count that q is being accessed by tx
+                                acount[q] += 1;
+                        }
+                }
+        }
+        return acount;
+}
+
+static void add_total_constraints(
+        VarMapper& vars,
+        const ResourceSharingInfo& info,
+        const TaskInfo& ti,
+        LinearProgram& lp,
+        unsigned int num_procs)
+{
+        // one constraint for each resource
+        hashmap<unsigned int, LinearExpression *> constraints;
+        LinearExpression *exp;
+
+        foreach_task_except(info.get_tasks(), ti, tx)
+        {
+                unsigned int t = tx->get_id();
+
+                //for all requests accessed by tx
+                foreach(tx->get_requests(), request)
+                {
+                        unsigned int q = request->get_resource_id();
+
+                        if (constraints.find(q) == constraints.end())
+                                constraints[q] = new LinearExpression();
+                        exp = constraints[q];
+                        foreach_request_instance(*request, ti, v)
+                        {
+                                unsigned int var_id;
+                                var_id = vars.lookup(t, q, v, BLOCKING_SOB);
+                                exp->add_var(var_id);
+                        }
+                }
+        }
+
+        // add each per-resource constraint
+        foreach(constraints, it) {
+                unsigned int bound = ti.get_num_requests(it->first);
+                bound *= (2 * num_procs - 1);
+                lp.add_inequality(it->second, bound);
+        }
+}
+
+
+static void add_remote_cluster_constraints(
+        VarMapper& vars,
+        const ResourceSharingInfo& info,
+        const TaskInfo& ti,
+        LinearProgram& lp,
+        AccessCounts& acount,
+        unsigned int num_procs,
+        unsigned int cluster_size)
+{
+        // one constraint for each cluster and each resource
+        hashmap<unsigned int, hashmap<unsigned int, LinearExpression *> > cluster_c;
+        LinearExpression *exp;
+
+        foreach_remote_task(info.get_tasks(), ti, tx)
+        {
+                unsigned int t = tx->get_id();
+                unsigned int c = tx->get_cluster();
+
+                hashmap<unsigned int, LinearExpression *> &constraints = cluster_c[c];
+
+                //for all requests accessed by tx
+                foreach(tx->get_requests(), request)
+                {
+                        unsigned int q = request->get_resource_id();
+
+                        if (constraints.find(q) == constraints.end())
+                                constraints[q] = new LinearExpression();
+                        exp = constraints[q];
+
+                        foreach_request_instance(*request, ti, v)
+                        {
+                                unsigned int var_id;
+                                var_id = vars.lookup(t, q, v, BLOCKING_SOB);
+                                exp->add_var(var_id);
+                        }
+                }
+        }
+
+        // add each per-resource constraint
+        foreach(cluster_c, ct) {
+                assert(ct->first != ti.get_cluster());
+                foreach(ct->second, it) {
+                        unsigned int bound  = ti.get_num_requests(it->first);
+                        unsigned int q = it->first;
+                        if (acount[q] <= 2 * cluster_size) {
+                                // FQ-only case
+                                bound *= acount[q];
+                        } else {
+                                // PQ case
+                                bound *= (cluster_size + num_procs);
+                        }
+                        lp.add_inequality(it->second, bound);
+                }
+        }
+}
+
+static void add_local_cluster_constraints(
+        VarMapper& vars,
+        const ResourceSharingInfo& info,
+        const TaskInfo& ti,
+        LinearProgram& lp,
+        AccessCounts& acount,
+        unsigned int cluster_size)
+{
+        foreach_local_task_except(info.get_tasks(), ti, tx)
+        {
+                unsigned int t = tx->get_id();
+                //for all requests accessed by tx
+                foreach(tx->get_requests(), request)
+                {
+                        unsigned int q = request->get_resource_id();
+                        LinearExpression *exp = new LinearExpression();
+
+                        foreach_request_instance(*request, ti, v)
+                        {
+                                unsigned int var_id;
+                                var_id = vars.lookup(t, q, v, BLOCKING_SOB);
+                                exp->add_var(var_id);
+                        }
+                        unsigned int bound = ti.get_num_requests(q);
+                        if (acount[q] > 2 * cluster_size)
+                                bound *= 2; // PQ case
+                        lp.add_inequality(exp, bound);
+                }