Relational MM: Cluster LMust

[michael-schwarz]

Re-creates #1555 but targeting master this time.

Currently, LMust is unclustered even when clusters are employed. This leads to precision loss compared to the unclustered variant when:

• Values are published to a mutex a for some clusters only
• a is added to LMust
• Upon lock(a), V.mutex_inits is not consulted for any cluster, as a is in LMust

However, V.mutex_inits should still be consulted for clusters that have not been published yet.

This also clusters LMust and adds a regression test for this behavior.

c.f. #1551

[sim642]

However, V.mutex_inits should still be consulted for clusters that have not been published yet.

This PR is marked as a precision improvement, but why isn't this a soundness matter?

[michael-schwarz]

This PR is marked as a precision improvement, but why isn't this a soundness matter?

It in fact is. I added another regression test for which master currently is unsound.