Compilation fails with thread safety errors in arena.rs

[younes-io]

When using scryer-prolog as a dependency with default-features = false, compilation fails with thread safety errors in arena.rs. The error occurs with Rust 1.83.0.

error[E0277]: `*const u8` cannot be shared between threads safely
   --> src/arena.rs:67:31
    |
67  |     static GLOBAL_ATOM_TABLE: RwLock<Weak<F64Table>> = RwLock::new(Weak::new());
    |                               ^^^^^^^^^^^^^^^^^^^^^^ `*const u8` cannot be shared between threads safely

Reproduction:

1. Create new Rust project
2. Add dependency:

[dependencies.scryer-prolog]
default-features = false
git = "https://github.com/mthom/scryer-prolog"
branch = "master"

3. Run cargo build

Environment:

• Rust: 1.83.0
• OS: Ubuntu 22.04
• Architecture: x86_64

Is this normal? What am I missing?

[younes-io]

This is really blocking :/ (I spent hours and unfortunately, I didn't find documentation that would "guide" newcomers to execute a simple basic, boilerplate, properly, without errors), then iterate on that

[Skgland]

I think this might be related to a soundness fix in the arcu dependencies your lockfile likely picked up the fixed version 0.1.2, while scryer itself still has 0.1.1 in its lockfile.
The Sync & Send bounds were too lax.

I tested it localy and master build but running cargo update arcu breaks the build.

It looks like the F64Table got caught in the soundness fix as RawBlock<F64Table> is not Sync & Send
and such the F64Table is no longer Send & Sync and cannot be stored in a static anymore.

@adri326 you were working on the atom table in #2736 and reported the issue in arcu do you maybe have some input on how to fix the F64Table?

It looks like AtomTable gets away with this as it manually implements Sync and Send.

[adri326]

You did yank 0.1.1, so that makes sense. The current implementation of F64Table doesn't look to be thread-safe, given that there is no explicit inter-thread happens-before relationship between a write to the RawBlock and a read from another thread, but in practice this can only be exploited to trigger a data race through an invalid heap cell, which can already trigger UB as F64Table doesn't do much bounds checking.

We could just manually implement Sync and Send; in the future I would like to refactor F64Table to be a lot less unsafe anyways.

[Skgland]

F64Table has update which is a Mutex that is used to synchronize allocations in the RawBlock similar to what AtomTable does.

[adri326]

That part is sound, yeah. The only part where I struggled to prove thread-safety (at least for AtomTable) is in the case where one thread is updating the table and another thread is trying to read from it, since there is a risk that it will attempt to read the newly-created entry, which would be a data race. But the only way for the second thread to read that hitherto unused memory is for it to either use an invalid offset, or to have synchronized with the first thread.

[Skgland]

You did yank 0.1.1, so that makes sense.

Even if I didn't yank it, cargo would pull in the latest semver compatible version of arcu when using scryer as a dependency. As a soundness fix I decided to not treat this breaking change as a major change.

all major changes are breaking, but not all breaking changes are major.
- Rust RFC 1105

[Skgland]

That part is sound, yeah. The only part where I struggled to prove thread-safety (at least for AtomTable) is in the case where one thread is updating the table and another thread is trying to read from it, since there is a risk that it will attempt to read the newly-created entry, which would be a data race. But the only way for the second thread to read that hitherto unused memory is for it to either use an invalid offset, or to have synchronized with the first thread.

The atomic operations in the replace of the hash_set and offsets tables should guarantee that the write to the raw block happens before, so that all readers that read the new values of those must also see the write to the raw block. As such it should either not find the atom in the old hash_set or offset table or it has the new tables and therefore must also have witnessed the write to the raw block.

[Skgland]

Given that we came to the conclusion that it should be sound even though scryer currently misses some Send/Sync impl that would prove this to the type system with the fixed arcu version.

For now a workaround would be to downgrade arcu to the yanked version e.g. via cargo update arcu --precise 0.1.1