Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix(engine/deps): preserve definitions order whenever possible #1151

Draft
wants to merge 2 commits into
base: main
Choose a base branch
from

Conversation

W95Psp
Copy link
Collaborator

@W95Psp W95Psp commented Nov 28, 2024

In most of the backends, a top-level definition should come prior to it's use. This is not true in Rust.

Thus, we need to sort the items so that item a comes before it is used in another item b.

We used to do that with a topological sort with the ocamlgraph library. But since this topological sort operated on a graph, we were loosing the original order of items.

This commit now:

  • construct a the transtive closure of the dependency graph
  • use this closure to stable sort the items

The comparison function is defined as follows (g denotes the transitive closure):

  1. if there is an edge a ⟶ b in g and an edge b ⟶ a, we are in a recursive bundle, hence we return 0: a equals b
  2. if there is an edge a ⟶ b in g, we return -1
  3. if there is an edge b ⟶ a in g, we return 1
  4. otherwise there is no relation between a and b, we return 0

The run for this PR on libcrux is there:

@W95Psp W95Psp marked this pull request as draft November 28, 2024 10:21
@W95Psp W95Psp force-pushed the fix-item-order-711-transitive-closure branch 2 times, most recently from 1ed3e2a to 7041ef6 Compare November 28, 2024 10:24
@franziskuskiefer
Copy link
Member

@W95Psp please reference the issue that this is closing

@franziskuskiefer franziskuskiefer linked an issue Nov 28, 2024 that may be closed by this pull request
@karthikbhargavan
Copy link
Contributor

#771

In most of the backends, a top-level definition should come prior to it's use.
This is not true in Rust.

Thus, we need to sort the items so that item `a` comes before it is
used in another item `b`.

We used to do that with a topological sort with the ocamlgraph
library. But since this topological sort operated on a graph, we were
loosing the original order of items.

This commit now:
 - construct a the transtive closure of the dependency graph
 - use this closure to stable sort the items

The comparison function is defined as follows (`g` denotes the transitive closure):
 1. if there is an edge `a ⟶ b` in `g` and an edge `b ⟶ a`, we are in a recursive bundle, hence we return `0`: `a` equals `b`
 2. if there is an edge `a ⟶ b` in `g`, we return `-1`
 2. if there is an edge `b ⟶ a` in `g`, we return `1`
 2. otherwise there is no relation between `a` and `b`, we return `0`
@W95Psp W95Psp force-pushed the fix-item-order-711-transitive-closure branch from 7041ef6 to aa33ea4 Compare January 14, 2025 15:06
@W95Psp
Copy link
Collaborator Author

W95Psp commented Jan 14, 2025

@karthikbhargavan
Copy link
Contributor

I hit this issue again yesterday when working on Bertie. Things were reordered with every change I made to some modules, for no good reason. I believe it also makes it hard to diff and debug the effect of engine changes (since the order change would make the diffs look much bigger than they are). So I encourage converting this into a reviewable PR whenever some other work item needs it.

@maximebuyse
Copy link
Contributor

I tried fixing this PR today. The first problem with it is the following:

fn f() {h()}

fn g() {}

fn h(){f()}

Open this code snippet in the playground
In this case f and h don't get grouped together because all elements have a comparison result of 0. But we need f and h to be together because they are mutually recursive. I fixed that by grouping them afterwards (that's not too complicated). But there is a second more complicated problem:

fn no_dependency_1() {}

fn f() {g()}

fn no_dependency_2() {}

fn g() {}

Open this code snippet in the playground
This doesn't work well because the implementation of List.stable_sort in ocaml needs the relation to be transitive and here no_dependency_2 = f and no_dependency_2 = g but f != g which so List.stable_sort lets things in the same order instead of moving f after g.

This means we can either implement our own sort that solves this issue (something like https://blog.gapotchenko.com/stable-topological-sort). Or use the solution of #1140 (using ocamlgraph stable topological sort with the original ordering passed as a comparison function). Note that the specs of this are a bit different from what we want (it doesn't guarantee to keep cycles together), but the implementation corresponds to what we want (but we should make sure that this doesn't change).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Engine: dependencies: the sorting seems unstable
4 participants