add causal order generator #2
Conversation
src/c3py/history.py
Outdated
| self.poset.order_try(f"{process}.{i + 1}", f"{process}.{i + 2}") | ||
|
|
||
| # co = (po U wr)^+ | ||
| def causal_order(self): |
There was a problem hiding this comment.
| def causal_order(self): | |
| def causal_order(self) -> Self: |
src/c3py/history.py
Outdated
| self.poset.order_try(f"{process}.{i + 1}", f"{process}.{i + 2}") | ||
|
|
||
| # co = (po U wr)^+ | ||
| def causal_order(self): |
There was a problem hiding this comment.
Perhaps you want a separate method for creating wr relation?
src/c3py/history.py
Outdated
| self.poset.order_try(f"{process}.{i + 1}", f"{process}.{i + 2}") | ||
|
|
||
| # co = (po U wr)^+ | ||
| def causal_order(self): |
There was a problem hiding this comment.
I don't want to add this causal_order method on History because this method only makes sense for histories of read/write memory. I think the easiest approach would be to make a subclass WRMemoryHistory that extends History and move this method there.
src/c3py/history.py
Outdated
|
|
||
| arg = op1.arg | ||
| ret = op1.ret | ||
| for id2, op2 in self.label.items(): |
There was a problem hiding this comment.
this inner loop makes the function
src/c3py/history.py
Outdated
| ret = op1.ret | ||
| for id2, op2 in self.label.items(): | ||
| if op2.method == "wr" and op2.arg == (arg, ret): | ||
| ch.poset.link(id2, id1) |
There was a problem hiding this comment.
It's my fault for not explicitly stating this, but currently, the graph (G) in the Poset class maintains two invariants (that comes from the definition of strong partial order).
First, the graph must be acyclic. This is to keep the relation irreflexive.
Second, the graph must be transitive closure. That is, if there is a path from a to b and b to c, there must also be an edge from a to c.
I'm fine with violating the property temporarily, but I have a feeling that we should NOT return an instance of Poset that is actually not a partial order.
I would probably change the function to def make_co(self) -> Self | None and return None if there is a cycle in the resulting poset. You probably don't need to check every time you add an edge and just need to check once at the end.
You also want to make sure the returned graph is transitive. You should be able to use a library function from networkx.
|
I created a new branch, |
add is_write_co_init_read method to WRMemoryHistory class
- add more tests for WRMemoryHistory class - check ThinAirRead in WRMemoryHistory.make_co
remove unnecessary if statement
2 participants
とりあえず一段階目としてco = (po + wr)+の定義に従ってcoを生成できるようにしてみました