runtimeverification / runtimeverification/llvm-backend
GC-BUG: Execution aborts while collecting old generation when using `free_all_kore_mem` in a few tests.
Nobody has claimed this yet.
- Dominant language
- C++
- Stars
- 43
- Forks
- 22
- PR merge metrics
- No merged PRs in 30d
Description
We observed that, while the new implementation of free_all_kore_mem looks more accurate from what it's supposed to do, we're now experiencing a segmentation fault when collecting the old generation in kore_collect.
The reason seems to be that the oldspace allocation_ptr is points to a memory position after the end of the oldspace, and thus, we can't correctly collect it. It's still uncertain why this happens, and the error seems to happen non-deterministically, probably because the program is executed using a pool of threads that (apparently) randomly switch threads during the execution of the program.
For now, the short-term solution is to not call munmap_arena_and_reset on the oldspace inside the free_all_kore_mem function, but we have to take a look into this issue GC issue later.
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start by reproducing the segmentation fault in the tests that use free_all_kore_mem, focusing on kore_collect and the oldspace allocation_ptr. Read the interactions between free_all_kore_mem and munmap_arena_and_reset, including the threaded execution context. Done means old-generation collection no longer aborts nondeterministically while preserving correct oldspace cleanup.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- cpp
- Domain
- backend, compilers
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 35/100