Document partial_order_concurrency [DOC-140] #4087

xbauch · 2019-02-05T15:27:31Z

This PR is only a part of DOC-140. There are no functional changes to the code.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig · 2019-02-05T15:34:58Z

src/goto-symex/partial_order_concurrency.h

+  /// Build identifier for the read/write clock variable
+  /// \param e: either shared read or shared write event
+  /// \param axiom: the clock variable to be used
+  /// \return irep id representing the clock variable of the event


I'd use "Identifier" instead of "irep id"

tautschnig · 2019-02-05T15:38:11Z

src/goto-symex/partial_order_concurrency.h

-  // produces the symbol ID for an event
+  /// Produce the symbol ID for an event
+  /// \param event: SSA step for the event
+  /// \return identifier of the lhs


I'd drop "of the lhs"

tautschnig · 2019-02-05T15:38:38Z

src/goto-symex/partial_order_concurrency.h

-  // produces an address ID for an event
+  /// Produce an address ID for an event
+  /// \param event: SSA step for the event
+  /// \return identifier of the lhs (without L2)


I'd say "L1-renamed identifier"

xbauch · 2019-02-05T15:47:43Z

@tautschnig Thanks for the quick review, I rewrote the documentation as suggested.

danpoe · 2019-02-05T16:03:58Z

src/goto-symex/partial_order_concurrency.h

@@ -35,6 +38,10 @@ class partial_order_concurrencyt:public messaget
    AX_PROPAGATION=8
  };

+  /// Build identifier for the read/write clock variable
+  /// \param e: either shared read or shared write event
+  /// \param axiom: the clock variable to be used


I think this parameter indicates the axiom that the resulting clock id is part of. Would that be right @tautschnig?

I agree; should I make it explicit in the description?

Yes, I think we should make it explicit for all the appearances of axiom.

danpoe · 2019-02-05T16:04:31Z

src/goto-symex/README.md

+
+\section Concurrency
+
+\subsection Partial Order Reduction


I'd name it just Partial Order Concurrency as it's not really partial order reduction.

You mean that its used to implement memory models but the ordering is never used for reduction?

Cf. http://www.kroening.com/papers/cav2013-wpo.pdf

It's a different technique. The encoding starts with unconstrained reads (i.e., with shared reads essentially being nondet), and then additional constraints are added to make the model stronger to yield e.g. TSO or SC.

peterschrammel · 2019-02-05T16:24:31Z

src/goto-symex/README.md

+
+\section Concurrency
+
+\subsection Partial Order Reduction


Cf. http://www.kroening.com/papers/cav2013-wpo.pdf

peterschrammel · 2019-02-05T16:26:10Z

src/goto-symex/partial_order_concurrency.h

  symbol_exprt clock(event_it e, axiomt axiom);
+
+  /// Initialise the __clock_type__ so that it can be used to number events


Well I guess it is called Oxford spelling after all. Spelling changed.

xbauch · 2019-02-05T16:38:03Z

I see, so the partial ordering is used to replace thread interleaving rather than reduce it. I changed the sub-section title in the readme.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 0f4d498).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99823236

xbauch requested review from kroening, peterschrammel and tautschnig as code owners February 5, 2019 15:27

tautschnig approved these changes Feb 5, 2019

View reviewed changes

xbauch force-pushed the docu/partial_order_concurrency branch from 40f0612 to a367fd5 Compare February 5, 2019 15:44

danpoe reviewed Feb 5, 2019

View reviewed changes

peterschrammel approved these changes Feb 5, 2019

View reviewed changes

peterschrammel assigned xbauch Feb 5, 2019

xbauch force-pushed the docu/partial_order_concurrency branch from a367fd5 to d4542d4 Compare February 5, 2019 16:32

peterschrammel added the documentation label Feb 5, 2019

Add documentation to goto-symex/partial_order_concurrency

0f4d498

xbauch force-pushed the docu/partial_order_concurrency branch from d4542d4 to 0f4d498 Compare February 5, 2019 17:29

allredj reviewed Feb 5, 2019

View reviewed changes

tautschnig merged commit 3fe7c67 into diffblue:develop Feb 5, 2019

xbauch deleted the docu/partial_order_concurrency branch June 10, 2019 12:28

		symbol_exprt clock(event_it e, axiomt axiom);

		/// Initialise the __clock_type__ so that it can be used to number events

Document partial_order_concurrency [DOC-140] #4087

Document partial_order_concurrency [DOC-140] #4087

Uh oh!

Conversation

xbauch commented Feb 5, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

xbauch commented Feb 5, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

xbauch commented Feb 5, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!