Implement weak partial ordering (WPO) of the graph for concurrent fixpoint iteration. #5

skkeem · 2019-10-28T02:19:15Z

This implements the Weak Partial Ordering (WPO) of a graph that generalizes the WTO.
It can be used to implement concurrent fixpoint iteration algorithms.
It is implemented in an iterative style so that it does not stack overflow during the WPO construction.

Test cases are added, including the cases for the irreducible graphs.
Ran clang-format to clean up the codes.

Publications:

Sung Kook Kim, Arnaud J. Venet, and Aditya V. Thakur. Deterministic Parallel Fixpoint Computation. To appear in POPL 2020
preprint: arXiv:1909.05951

facebook-github-bot

@int3 has imported this pull request. If you are a Facebook employee, you can view this diff on Phabricator.

int3

Still working through the paper, but this looks pretty awesome. Thank you!!

int3 · 2019-10-28T12:24:21Z

include/WeakPartialOrdering.h

+ private:
+  // WPO nodes.
+  std::vector<WpoNodeT> m_nodes;
+  // Top level nodes. Nodes that are outside of any component.


Suggested change

// Top level nodes. Nodes that are outside of any component.

// Top level nodes: Nodes that are outside of any component.

int3 · 2019-10-29T19:33:39Z

include/WeakPartialOrdering.h

+  }
+
+ private:
+  // Construct auxilary data-structures.


s/auxilary/auxiliary/

int3 · 2019-10-29T19:36:54Z

include/WeakPartialOrdering.h

+  bool is_widening_point() const { return m_widen; }
+
+ private:
+  // Add successor.


No need for comments that state things that are obvious from the code :)

int3 · 2019-10-29T19:39:31Z

test/WeakPartialOrderingTest.cpp

+
+using WpoIdx = uint32_t;
+
+class SimpleGraph2 final {


Could you factor SimpleGraph from the WeakTopologicalOrderingTest into a separate file and reuse it here?

int3 · 2019-10-29T19:43:47Z

test/WeakPartialOrderingTest.cpp

+    int i = 0;
+    std::ostringstream wto;
+    bool first = true;
+    while (!wl.empty()) {


This check-properties-and-print-wto-string code seems to be repeated across many tests... could it be factored out?

ssj933 · 2019-11-06T00:29:11Z

include/WeakPartialOrdering.h

+        worklist_h.pop_back();
+        for (auto p : m_non_back_preds[v]) {
+          auto rep_p = rep[dsets.find_set(p)];
+          auto it = nested_SCCs_h.find(rep_p);


nit: The it here will shadow the it in line 412.

int3 · 2019-11-08T01:42:11Z

We've decided to merge this as-is and do the fixups ourselves. Thanks for all your work @skkeem! We're super excited to productionize this :)

…point iteration. (#5) Summary: This implements the Weak Partial Ordering (WPO) of a graph that generalizes the WTO. It can be used to implement concurrent fixpoint iteration algorithms. It is implemented in an iterative style so that it does not stack overflow during the WPO construction. - Test cases are added, including the cases for the irreducible graphs. - Ran clang-format to clean up the codes. Publications: - Sung Kook Kim, Arnaud J. Venet, and Aditya V. Thakur. Deterministic Parallel Fixpoint Computation. To appear in POPL 2020 - preprint: [arXiv:1909.05951](https://arxiv.org/abs/1909.05951) Pull Request resolved: facebook/SPARTA#5 Reviewed By: yuxuanchen1997 Differential Revision: D18169499 Pulled By: int3 fbshipit-source-id: 64fcc87ce94b33c34fdbe89a327ebb7e99b64697

facebook-github-bot · 2019-11-08T04:11:45Z

@int3 merged this pull request in 862564b.

ssj933 · 2019-12-16T23:05:59Z

Hi @skkeem , I am not sure if the get_num_outer_preds(WpoIdx exit) funtion is the corresponding method for NumOuterSchedPreds in paper. As I found the result given for one of the node in the following graph doesn't seem to match expectation.

Construct a SimpleGraph2 using following codes:

SimpleGraph2 g;
g.add_edge("1", "12");
g.add_edge("1", "16");
g.add_edge("1", "18");
g.add_edge("1", "26");
g.add_edge("12", "45");
g.add_edge("12", "75");
g.add_edge("12", "46");
g.add_edge("16", "74");
g.add_edge("16", "75");
g.add_edge("18", "92");
g.add_edge("26", "93");
g.add_edge("45", "46");
g.add_edge("46", "47");
g.add_edge("47", "73");
g.add_edge("73", "74");
g.add_edge("73", "75");
g.add_edge("73", "73");
g.add_edge("74", "46");
g.add_edge("75", "45");
g.add_edge("92", "93");
g.add_edge("93", "45");
g.add_edge("93", "46");

WeakPartialOrdering<std::string> wpo(
    "1", [&g](const std::string& n) { return g.successors(n); }, false);

Traverse through the graph and print out get_num_outer_preds for exit nodes, and predecessors of each nodes. The result for exit node with NodeId "46" only have number for head node with NodeId "46". However in the component for exit node with NodeId "46", there is another node with NodeId "74", it have two predecessors in WPO, one is node with NodeId "16" which is outside of the component, another is node with NodeId "73" which is inside of the component, so I think get_num_outer_preds for exit node with NodeId "46" should have node with NodeId "74" have value 1 (but there is no value for node with NodeId "74").
(This could cause some node not been visited because the counter couldn't reach their num_preds after the component didn't stabilize and need to re-run. )

Thanks for your help!

skkeem · 2019-12-17T23:51:24Z

Hello @ssj933,

Thank you for bringing this to my attention.

wpo.get_num_outer_preds(x)[v] should be equal to NumOuterSchedPreds(v, x) in the paper.

As you have correctly pointed out, wpo.get_num_outer_preds(x_46)[74] (= NumOuterSchedPreds(74, x_46)) should be 1.

I have fixed the bug and added corresponding test cases in PR #7 .

Thank you.

skkeem added 2 commits October 25, 2019 16:50

Implement weak partial ordering (WPO)

bed5241

add comment describing the lifted in the test case

be6c8c3

facebook-github-bot added the CLA Signed Do not delete this pull request or issue due to inactivity. label Oct 28, 2019

facebook-github-bot reviewed Oct 28, 2019

View reviewed changes

int3 reviewed Oct 29, 2019

View reviewed changes

ssj933 reviewed Nov 6, 2019

View reviewed changes

facebook-github-bot closed this in 862564b Nov 8, 2019

facebook-github-bot added the Merged label Nov 8, 2019

arthaud mentioned this pull request Dec 17, 2019

Weak partial order implementation NASA-SW-VnV/ikos#156

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Implement weak partial ordering (WPO) of the graph for concurrent fixpoint iteration. #5

Implement weak partial ordering (WPO) of the graph for concurrent fixpoint iteration. #5

skkeem commented Oct 28, 2019

facebook-github-bot left a comment

int3 left a comment

int3 Oct 28, 2019

int3 Oct 29, 2019

int3 Oct 29, 2019

int3 Oct 29, 2019

int3 Oct 29, 2019

ssj933 Nov 6, 2019

int3 commented Nov 8, 2019

facebook-github-bot commented Nov 8, 2019

ssj933 commented Dec 16, 2019 •

edited

Loading

skkeem commented Dec 17, 2019

	// Top level nodes. Nodes that are outside of any component.
	// Top level nodes: Nodes that are outside of any component.

Implement weak partial ordering (WPO) of the graph for concurrent fixpoint iteration. #5

Implement weak partial ordering (WPO) of the graph for concurrent fixpoint iteration. #5

Conversation

skkeem commented Oct 28, 2019

facebook-github-bot left a comment

Choose a reason for hiding this comment

int3 left a comment

Choose a reason for hiding this comment

int3 Oct 28, 2019

Choose a reason for hiding this comment

int3 Oct 29, 2019

Choose a reason for hiding this comment

int3 Oct 29, 2019

Choose a reason for hiding this comment

int3 Oct 29, 2019

Choose a reason for hiding this comment

int3 Oct 29, 2019

Choose a reason for hiding this comment

ssj933 Nov 6, 2019

Choose a reason for hiding this comment

int3 commented Nov 8, 2019

facebook-github-bot commented Nov 8, 2019

ssj933 commented Dec 16, 2019 • edited Loading

skkeem commented Dec 17, 2019

ssj933 commented Dec 16, 2019 •

edited

Loading