Change sharing map so that leafs can be directly attached to internal nodes #4685

danpoe · 2019-05-21T19:11:59Z

Previously all leafs were stored in a linked list. However, this was unnecessary as collisions can occur only between nodes at the bottom of the tree. Now only leafs at the bottom are stored in a linked list, and all other leafs are direct successors of internal nodes.

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a 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.

danpoe · 2019-05-21T19:13:50Z

On a set of methods from Apache Tika, the sum of the runtimes of the sharing map methods (timing just those) improved by 28%. Overall symex was 7% faster.

smowton · 2019-05-22T09:07:34Z

src/util/sharing_map.h

-  typedef sharing_node_leaft<key_type, mapped_type> leaft;
-
-  typedef sharing_node_baset baset;
+  typedef sharing_nodet<key_type, mapped_type> innert;


(random line) commit message: where -> were :p

smowton

LGTM (at moderate depth, haven't walked through the algorithms in detail to make sure there are no missing cases). Surprised not to see any updates to the top-level docs for the data structure though?

smowton · 2019-05-22T09:08:51Z

src/util/sharing_node.h

@@ -70,14 +69,14 @@ const T *as_const(T *t)

 // Inner nodes (internal nodes or container nodes)


Comment out of date now there are 3 possibilities?

smowton · 2019-05-22T09:12:24Z

src/util/sharing_map.h

-
-    return lp;
-  }
+  leaft *get_leaf_node(const key_type &k);


(random line) commit message: leafs -> leaf

smowton · 2019-05-22T09:14:41Z

src/util/sharing_map.h


-    key >>= chunk;
+    if(ip->is_leaf())


These are mutually exclusive, right? If so use else if to clarify that.

smowton · 2019-05-22T09:14:53Z

src/util/sharing_map.h

+      continue;
+    }
+
+    if(ip->is_leaf())


smowton · 2019-05-22T09:15:04Z

src/util/sharing_map.h

+      num--;
+
+      return;
+    }

    if(ip->is_container())


tautschnig · 2019-05-22T11:57:47Z

src/util/sharing_map.h


  INVARIANT(
-    !value_equalt()(as_const(lp)->get_value(), m),
+    !value_equalt()(as_const(lp).get_value(), m),


Visual Studio complains that the use of as_const is ambiguous here. You might have add/use a static cast here.

Previously the leaf nodes were a separate type, and internal nodes and container nodes were represented by the same type. This changes the representation such that all nodes are represented by sharing_nodet. This will allow an internal node to directly point to a leaf node (instead of having to point to a container node which in turn points to a leaf node).

…haring map This adapts the methods for the case where a leaf can directly be attached to internal nodes.

Adapt get_view() and get_delta_view() for the case where a leaf node is directly attached to an internal node.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: e7a5cf1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112914521
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

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

…g ones The shape of a sharing map is now different than before, as now leafs can be directly attached to internal nodes. This adapts the various unit tests that check that the map has a certain shape.

Previously some methods returned a pointer but would never return nullptr. This changes their return type to references instead.

Previously there existed a separate leaft type. Now all nodes are of the type sharing_nodet<...> (of which nodet is an lias). This replaces all node types by nodet.

When destructt::destruct() of a small shared n-way pointer is called, it first determines the type of its pointee. For example, if the parameter pack Ts... is instantiated to T1, T2, T3, then it first checks if the pointer points to T3, then to T2, etc. Thus, the least checks are performed if it is most likely that the pointer points to an object of type T3, then T2, etc.

Update the documentation to reflect the fact that the sharing map is now a variable-height tree.

Since the sharing map is now a variable-height tree, the best case complexity of various operations has changed.

allredj

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

danpoe requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners May 21, 2019 19:11

danpoe force-pushed the feature/sharing-map-leafs branch from 4fd5b3d to 6ac45f2 Compare May 21, 2019 19:36

smowton reviewed May 22, 2019

View reviewed changes

smowton approved these changes May 22, 2019

View reviewed changes

danpoe force-pushed the feature/sharing-map-leafs branch 3 times, most recently from 8341802 to d4d4ca5 Compare May 22, 2019 10:45

tautschnig reviewed May 22, 2019

View reviewed changes

tautschnig assigned danpoe May 22, 2019

danpoe force-pushed the feature/sharing-map-leafs branch 2 times, most recently from e7a5cf1 to 8c2b37e Compare May 23, 2019 10:32

danpoe added 3 commits May 23, 2019 12:23

Adapt methods for finding, erasing, and inserting elements into the s…

31988af

…haring map This adapts the methods for the case where a leaf can directly be attached to internal nodes.

Adapt iteration over the sharing map

43268ed

Adapt get_view() and get_delta_view() for the case where a leaf node is directly attached to an internal node.

allredj reviewed May 23, 2019

View reviewed changes

danpoe force-pushed the feature/sharing-map-leafs branch from 12e4945 to 872f203 Compare May 23, 2019 11:33

allredj reviewed May 23, 2019

View reviewed changes

danpoe force-pushed the feature/sharing-map-leafs branch from 872f203 to c7126b8 Compare May 23, 2019 12:45

danpoe added 7 commits May 23, 2019 14:26

Add new unit tests which check the shape of the map and adapt existin…

a2f32bf

…g ones The shape of a sharing map is now different than before, as now leafs can be directly attached to internal nodes. This adapts the various unit tests that check that the map has a certain shape.

Remove obsolete method is_singular() in sharing_mapt

4e0577a

Use emplace() in sharing_nodet

794bd8b

Return reference from methods that cannot return a nullpointer

37c3439

Previously some methods returned a pointer but would never return nullptr. This changes their return type to references instead.

Use type nodet to represent sharing map nodes

900d29c

Previously there existed a separate leaft type. Now all nodes are of the type sharing_nodet<...> (of which nodet is an lias). This replaces all node types by nodet.

Update high-level sharing map documentation

618deb4

Update the documentation to reflect the fact that the sharing map is now a variable-height tree.

Update best case complexity of sharing map operations

d438341

Since the sharing map is now a variable-height tree, the best case complexity of various operations has changed.

danpoe force-pushed the feature/sharing-map-leafs branch from c7126b8 to d438341 Compare May 23, 2019 13:26

danpoe merged commit 7734b53 into diffblue:develop May 23, 2019

allredj reviewed May 23, 2019

View reviewed changes

danpoe deleted the feature/sharing-map-leafs branch June 2, 2020 17:08

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Change sharing map so that leafs can be directly attached to internal nodes #4685

Change sharing map so that leafs can be directly attached to internal nodes #4685

Uh oh!

danpoe commented May 21, 2019 •

edited

Loading

Uh oh!

danpoe commented May 21, 2019

Uh oh!

smowton May 22, 2019

Uh oh!

smowton left a comment

Uh oh!

smowton May 22, 2019

Uh oh!

smowton May 22, 2019

Uh oh!

smowton May 22, 2019

Uh oh!

smowton May 22, 2019

Uh oh!

smowton May 22, 2019

Uh oh!

tautschnig May 22, 2019

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

		@@ -70,14 +69,14 @@ const T as_const(T t)

		// Inner nodes (internal nodes or container nodes)

Change sharing map so that leafs can be directly attached to internal nodes #4685

Change sharing map so that leafs can be directly attached to internal nodes #4685

Uh oh!

Conversation

danpoe commented May 21, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

danpoe commented May 21, 2019

Uh oh!

smowton May 22, 2019

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

smowton May 22, 2019

Choose a reason for hiding this comment

Uh oh!

smowton May 22, 2019

Choose a reason for hiding this comment

Uh oh!

smowton May 22, 2019

Choose a reason for hiding this comment

Uh oh!

smowton May 22, 2019

Choose a reason for hiding this comment

Uh oh!

smowton May 22, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig May 22, 2019

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

danpoe commented May 21, 2019 •

edited

Loading