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

Improve safety of atom tables and RawBlock #2727

Open
wants to merge 4 commits into
base: rebis-dev
Choose a base branch
from

Conversation

adri326
Copy link
Contributor

@adri326 adri326 commented Dec 29, 2024

The safety of the operations defined for Atom and RawBlock relied until now on undocumented and unasserted properties of the inputs and the environment.

For instance, the following (dubious) library prolog code triggers undefined behavior:

dubious_load_library(Path) :- open(Path, read, Stream, []), '$load_library_as_stream'(Stream, _, _).

This PR aims to lessen the chance of someone inadvertently causing undefined behavior from an incorrect usage of Atom or RawBlock, by making the following changes:

  • Turn RawBlockTraits::align() into a constant, to enforce the invariant that it must be constant. This should also slightly improve performance.
  • Fix RawBlock::alloc not actually aligning the size to T::align(), causing potential UB (all call sites were already aligning the size themselves).
  • Assert that atom pointers are within the bounds of their atom table and are correctly aligned (makes it so that the previous code sample now panics instead of segfaulting).
  • Don't create an invalid, temporary AtomData before the right metadata for its fat pointer is obtained.
  • Assert at compile time that AtomData has the expected representation.
  • Encapsulate accesses to RawBlock, to reduce the amount of code that needs to uphold its invariants. The raw accesses are replaced with functions with both checked and unchecked variants.
  • Replace UnsafeCell with Cell in RawBlock, as the previous code did not need to hand out mutable borrows to ptr. RawBlock is still not Sync.
  • Rename ptr to head and store it as an offset from base, to reduce the number of pointer operations to keep track of.
  • Document the invariants of AtomData and RawBlock.
  • Informally prove the safety of operations within AtomData and RawBlock.

I'm well aware that these are a lot of changes. I split them into multiple commits to make it possible to pull out changes into a future PR if needs be :)

@triska
Copy link
Contributor

triska commented Dec 29, 2024

Thank you so much for working on this!

One question I have regarding these changes: Would it be better to apply them directly to the upcoming rebis-dev development branch, so that the future merge is easier?

Please see the announcement and discussion at: #2569

@adri326
Copy link
Contributor Author

adri326 commented Dec 29, 2024

The rebase to rebis-dev shouldn't be too hard

@adri326 adri326 changed the base branch from master to rebis-dev December 29, 2024 18:42
@triska
Copy link
Contributor

triska commented Dec 29, 2024

@bakaq: I would greatly appreciate if you could take a look at these impressive changes!

Copy link
Contributor

@bakaq bakaq left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Very nice! Not much to point out that you haven't already acknowledged in TODO comments.

src/machine/stack.rs Outdated Show resolved Hide resolved
src/machine/stack.rs Outdated Show resolved Hide resolved
@adri326
Copy link
Contributor Author

adri326 commented Dec 30, 2024

I'm not sure why AndFrame::index behaves like a 1-indexed array, but I've added assertions in stack.rs where they were easy to add, and otherwise added TODOs to come back later to, as I don't want to blow out the complexity of this PR.

I would like to suggest in a subsequent PR a way to make the API of AtomTable fully safe, but those changes will need to be built on top of this PR's changes :)

@triska
Copy link
Contributor

triska commented Dec 30, 2024

@adri326: This looks awesome, thank you so much for all these impressive contributions!

src/arena.rs Show resolved Hide resolved
@mthom
Copy link
Owner

mthom commented Jan 12, 2025

Looks like there are some module access restrictions preventing the CI tests from passing.

@adri326
Copy link
Contributor Author

adri326 commented Jan 12, 2025

Those were fixed by #2735 iirc

@triska
Copy link
Contributor

triska commented Jan 12, 2025

@adri326 is there a way to rerun the CI tests for this PR? One easy way may be to amend the topmost commit with --date=now and then force-push.

@adri326
Copy link
Contributor Author

adri326 commented Jan 12, 2025

Did a rebase, the one failing test case is fixed in #2759, but you can run the tests locally with --no-fail-fast to let it go through all of the other ones.

I should probably squash those commits down, too.

@triska
Copy link
Contributor

triska commented Jan 12, 2025

Mark referred to the CI tests which we see on github at the end of this PR discussion, they still fail:

image

You can click on the tests to see more information.

This notably tightens assertions in RawBlock::get to require indices to be less than head.
A special case for Machine::get_clause_p, as it needs to read a dangling stack frame.

Switch `RawBlock.head` to be a Cell to reduce the number of invariants and be closer to
being thread-safe.
- Fix miri warning about pointer->integer->pointer cast in stack.rs
- Panic if Stack::truncate is called with an unaligned value
- Add assertions in stack.rs and TODOs for leftover unsafe operations
@adri326
Copy link
Contributor Author

adri326 commented Jan 12, 2025

@triska that's what I also understood. What I meant earlier was that the CI passing depends on #2759 (as of now, the same error in the CI occurs in rebis-dev), but the changes of this PR are themselves independent.

In the meantime, I've reorganised/squashed the commits for them to not be a mess anymore :)

As proof, you can see that the tests pass if you locally cherry-pick the fix from #2759:

git cherry-pick 2546976
cargo test
# All tests pass

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.

5 participants