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

FreeBSD: implement support for pthread synchronization primitives #3571

Open
RalfJung opened this issue May 5, 2024 · 0 comments
Open

FreeBSD: implement support for pthread synchronization primitives #3571

RalfJung opened this issue May 5, 2024 · 0 comments
Labels
A-concurrency Area: affects our concurrency (multi-thread) support A-freebsd Area: affects our FreeBSD target support A-shims Area: This affects the external function shims C-enhancement Category: a PR with an enhancement or an issue tracking an accepted enhancement E-good-second-issue A good issue to pick up if you've already seen some parts of Miri, mentoring is available

Comments

@RalfJung
Copy link
Member

RalfJung commented May 5, 2024

We currently don't support the pthread synchronization primitives on FreeBSD. And it turns out that supporting them will require some refactoring of how we implement those primitives: on FreeBSD, pthread_mutex_t et al are just a pointer to the actual data. That means on a 32bit system they are only 4 bytes large, which is not large enough for us to store the data we need to store directly in the pthread_mutex_t.

So we need to do what likely the FreeBSD implementation also does, and allocate some memory to store the mutex data in, making the mutex itself just a pointer to that memory. We could do that only on FreeBSD and keep things unchanged on all other targets, but I see no reason to carry two implementations -- let's just switch everything over. That will also give us detection of leaks or double-frees for these constructs, since we'd leak / double-free their backing memory.

The static initializer is a null pointer, so all mutex operations will have to lazily allocate the backing memory. (That can replace the current scheme of lazily assigning a mutex ID.) This has to happen atomically since multiple threads could be trying to acquire the same lock that was not previously initialized.

There's a little complication on Linux, which has static initializers for non-default mutex kinds. The lazy allocation will have to carry over the mutex kind to the newly allocated memory.

@RalfJung RalfJung added C-enhancement Category: a PR with an enhancement or an issue tracking an accepted enhancement A-shims Area: This affects the external function shims E-good-first-issue A good way to start contributing, mentoring is available A-concurrency Area: affects our concurrency (multi-thread) support A-freebsd Area: affects our FreeBSD target support E-good-second-issue A good issue to pick up if you've already seen some parts of Miri, mentoring is available and removed E-good-first-issue A good way to start contributing, mentoring is available labels May 5, 2024
@RalfJung RalfJung changed the title FreeBSD: implement support for pthread synchronization primitives Android/FreeBSD: implement support for pthread synchronization primitives May 19, 2024
@RalfJung RalfJung changed the title Android/FreeBSD: implement support for pthread synchronization primitives FreeBSD: implement support for pthread synchronization primitives May 19, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-concurrency Area: affects our concurrency (multi-thread) support A-freebsd Area: affects our FreeBSD target support A-shims Area: This affects the external function shims C-enhancement Category: a PR with an enhancement or an issue tracking an accepted enhancement E-good-second-issue A good issue to pick up if you've already seen some parts of Miri, mentoring is available
Projects
None yet
Development

No branches or pull requests

1 participant