Vec.h SEGFAULT

[Ricardo Marques]

Hi all,

I developed a parallel solver which includes clause and unit sharing.

However, I've noticed some bugs in the solver, namely in the vec structures.

With some debugging I concluded that if I do the assertion below the solver (very rarely) aborts.

unitLits.push (learntUnits[i][j]);

assert (unitLits.last() == learntUnits[i][j]);

The structures unitLits and ** learntUnits are of vec<Lit>

Shouldn't this assertion be always right?

Can anyone tell me why does this happen?

Thank you,

Ricardo Marques

[Mate Soos]

Dear Ricardo,

Is there any specific reason to use vec<> instead of std::vector<> in
your case? Are you aware of the differences? I think you would have less
trouble if you used std::vector<> -- it works in more cases.

I hope I have helped,

Mate

[Michael Tautschnig]

Hi,

> I developed a parallel solver which includes clause and unit sharing.
> However, I've noticed some bugs in the solver, namely in the vec structures.
> With some debugging I concluded that if I do the assertion below the solver
> (very rarely) aborts.
>

Does this also happen when you disable all the parallelism in your solver?

> unitLits.push (learntUnits[i][j]);
> assert (unitLits.last() == learntUnits[i][j]);
>
> The structures unitLits and ** learntUnits are of vec<Lit>
>
> Shouldn't this assertion be always right?
> Can anyone tell me why does this happen?
>

In all likelihood you are concurrently modifying unitLits or learntUnits.
Essentially two cases will cause this assertion to fail (assuming that i and j
aren't shared):

- Multiple threads execute unitLits.push (learntUnits[i][j]) before either of
them reaches the assertion.
- Another thread modifies learntUnits[i][j] before the assertion is tested.

Best,
Michael

[Ricardo Marques]

Problem Solved.

It turned out the problem was not concurrent access (the parallel implementation guarantees that each thread owns a index of the matrix for writting and the other threads reading), but the "capacity" function of the Vec structure, that uses realloc to resize the vector. Probably some accesses were made while this routine was being called, therefore the errors obtained.

Thank you all for your help,

Ricardo Marques