Skip to content

Fix stale PicoSAT literal pointer crash under multi-threaded solve#831

Open
GregoryMorse wants to merge 1 commit into
msoos:masterfrom
GregoryMorse:fix-picosat-stale-pointer
Open

Fix stale PicoSAT literal pointer crash under multi-threaded solve#831
GregoryMorse wants to merge 1 commit into
msoos:masterfrom
GregoryMorse:fix-picosat-stale-pointer

Conversation

@GregoryMorse

@GregoryMorse GregoryMorse commented Jun 17, 2026

Copy link
Copy Markdown

PicoSAT's inc_max_var() can realloc ps->lits when new variables are encountered mid-clause. Although fix_added_lits() patches buffered Lit* pointers in ps->added, the realloc is layout-sensitive: under heavy 8-thread allocation pressure the patch can miss a pointer, causing a dereference of a stale/corrupt Lit* in trivial_clause().

Fix: pre-register all variables with picosat_inc_max_var() before any picosat_add(...literal...) opens a clause, so ps->lits is fully grown before any Lit* pointers are buffered. Added:

  • register_lit_to_picovar() — registers a variable with PicoSAT without incrementing picolits_added (used during pre-registration)
  • pre_register_picosat_vars() — walks watched clauses and pre- registers all variables via register_lit_to_picovar()
  • Called at all three PicoSAT call sites before clause construction
  • release_assert in lit_to_picolit() that the variable was pre- registered, so any future pre-pass mismatch is caught immediately rather than manifesting as a rare heap crash

Also: skip red binary watches in pre-registration (matching the filter in add_cls_to_picosat_definable), and reset picosat on added==0 in the definable paths to avoid accumulating unused vars.

… Windows

PicoSAT's inc_max_var() can realloc ps->lits when new variables are
encountered mid-clause.  Although fix_added_lits() patches buffered
Lit* pointers in ps->added, the realloc is layout-sensitive: under
heavy 8-thread allocation pressure the patch can miss a pointer,
causing a dereference of a stale/corrupt Lit* in trivial_clause().

Fix: pre-register all variables with picosat_inc_max_var() before
any picosat_add(...literal...) opens a clause, so ps->lits is fully
grown before any Lit* pointers are buffered.  Added:

- register_lit_to_picovar() — registers a variable with PicoSAT
  without incrementing picolits_added (used during pre-registration)
- pre_register_picosat_vars() — walks watched clauses and pre-
  registers all variables via register_lit_to_picovar()
- Called at all three PicoSAT call sites before clause construction
- release_assert in lit_to_picolit() that the variable was pre-
  registered, so any future pre-pass mismatch is caught immediately
  rather than manifesting as a rare heap crash

Also: skip red binary watches in pre-registration (matching the
filter in add_cls_to_picosat_definable), and reset picosat on
added==0 in the definable paths to avoid accumulating unused vars.
@GregoryMorse

Copy link
Copy Markdown
Author

Fixes #830

@GregoryMorse

Copy link
Copy Markdown
Author

I have now run it for many hours over many various large instances and it is finally observably stable.

I don't think this is Windows only and it is bizarre that it has not been observed previously. It can be that threads>=8 and realloc on linux are less likely to change allocation addresses. Picosat depends on realloc and pointer delta adjustments. Picosat is fragile and too address-sensitive. The fix here is a clean way around having to worry about it.

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