Skip to content

Variables protected by mutex are incorrectly calculated #1712

@sim642

Description

@sim642
./regtest.sh 46 98 --enable dbg.print_protection

outputs

[Info][Race] Variable nothing2 read-write protected by 1 mutex(es): {f}
[Info][Race] Mutex f read-write protects 1 variable(s): {nothing2}
[Info][Race] Variable j read-write protected by 1 mutex(es): {f}

The first and third lines use the dynamically computed "mutexes protecting the variable" information: both are protected by f.
The second line uses the inverse information which is only computed during postsolving, but somehow it only lists nothing2, but should also list j.

I think this information is only used for dbg.print_protection and witness-generation, which is probably why it has gone unnoticed for so long.

PR #1631 identified that write:bool is used with different meanings but didn't reveal any issues arising from it, only confusion. I suspect this bug might actually be caused by the mixup.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions