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

Rewrite the tool #126

Merged
merged 6 commits into from
May 22, 2024
Merged

Rewrite the tool #126

merged 6 commits into from
May 22, 2024

Conversation

Ivan-Velickovic
Copy link
Collaborator

@Ivan-Velickovic Ivan-Velickovic commented May 21, 2024

This PR rewrites the entire Microkit tool from Python to Rust.

This was done for the following reasons:

  • The current tool was difficult to build from source. It took too long,
    did not have any cache for rebuilds, and sometimes would not reliably
    build/link as a static binary.
  • While perhaps not as extensive as C, Rust does have some verification
    tooling surrounding it, meaning it is possible for us to verify the
    Microkit tool in the future. Although at this time there are no
    concrete plans to verify the tool.

This rewrite, while not significantly reducing our dependencies in
general, does improve the situation. We are no longer dependent on
pyoxidizer, which was causing most of the issues with the tool.

We introduce a dependency on the Rust toolchain. The tool itself has
two dependencies (for XML parsing). No other dependencies are needed,
and it was a conscious decision to re-invent the wheel where the Rust
standard library was lacking (compared to the Python standard library).

The other programming languages considered for the rewrite were Zig and
Go. While they both have their benefits and costs (as does Rust), they were not
chosen due to them not being in any other seL4 Foundation supported projects
meaning that it could have been difficult to continue maintaining them
in the future.

The main cost of rewriting the tool in Rust is that it has
become slightly more complicated and harder to understand. This could potentially
result in a higher barrier to entry for contributors. However, most
contributions such as adding platform support will not need to touch the
tool.

@Ivan-Velickovic
Copy link
Collaborator Author

It should be noted that for the example programs that are in the repository, the rewritten tool produces the same binary as the current tool.

The only observable differences between the new tool and the current one is various bug fixes and improvements to error messages.

Other than that, there should be no observable differences to users.

@Ivan-Velickovic Ivan-Velickovic force-pushed the rs branch 4 times, most recently from 99edb1a to 7692356 Compare May 22, 2024 03:01
This commit rewrites the entire Microkit tool from Python to Rust.

This is was done for the following reasons:
* The current tool was difficult to build from source. It took too long,
  did not have any cache for rebuilds, and sometimes would not reliably
  build/link with musl.
* While perhaps not as extensive as C, Rust does have some verification
  tooling surrounding it, meaning it is possible for us to verify the
  Microkit tool in the future. Although at this time there are no
  concrete plans to verify the tool.

This rewrite, while not significantly reducing our dependencies in
general, does improve the situation. We are no longer dependent on
pyoxidizer, which was causing most of the issues with the tool.

We introduce a dependency on the Rust toolchain. The tool itself has
two dependencies (for XML parsing). No other dependencies are needed,
and it was a conscious decision to re-invent the wheel where the Rust
standard library was lacking (compared to the Python standard library).

The other programming languages considered for the rewrite were Zig and
Go. While they both have their benefits and costs (as does Rust), they
were not chosen due to them not being in any other seL4 Foundation
supported projects meaning that it could have been difficult to continue
maintaining the tool in the future.

The main cost of rewriting the tool in Rust is that it has undoubtedly
become more complicated and harder to understand. This could potentially
result in a higher barrier to entry for contributors. However, most
contributions such as adding platform support will not need to touch the
tool.

Signed-off-by: Ivan Velickovic <[email protected]>
Signed-off-by: Ivan Velickovic <[email protected]>
Signed-off-by: Ivan Velickovic <[email protected]>
Signed-off-by: Ivan Velickovic <[email protected]>
Because these are packed structures, we need to include the
other fields (even if we do not use them) for alignment.

Signed-off-by: Ivan Velickovic <[email protected]>
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.

1 participant