JetBrains / lincheck

Framework for testing concurrent data structures
Mozilla Public License 2.0
572 stars 33 forks source link

Support operations with multiple suspension points #122

Open alefedor opened 1 year ago

alefedor commented 1 year ago

See #121 for an example of Lincheck failing in the case of multiple suspension points per operation

btwilk commented 1 year ago

This restricts modular testing to using only a single submodule.

ndkoval commented 1 year ago

Supporting multiple suspensions is vital for #167

ndkoval commented 1 year ago

Please have a look at #143 for preliminary support in the runner. Let's support multiple suspensions ONLY in the runner, printing an error if multiple suspensions occur in the verification phase.

btwilk commented 1 year ago

Can you clarify whether support in only the runner would resolve #121 ?

ndkoval commented 1 year ago

@btwilk yes

ndkoval commented 4 months ago

Note: with allowing multiple suspensions only in the running phase, we need to check that at most one suspension occurs in the verification phase.