Introduce extended specs to allow wrapping command sequences

[polytypic]

See #510.

Contrary to what #510 concluded with, I decided to introduce

• an extended Spec signature, SpecExt,
• a module of default specs, SpecDefaults,
• and extended functors, STM_sequential.MakeExt, STM_domain.MakeExt, and STM_thread.MakeExt.

The reason for this is that introducing wrapped variants of the various functions produced by the functors would have roughly meant duplicating all of the functions. This approach is much more incremental and also potentially allows the Spec interface to the extended in the future.

The idea is that one always uses the SpecDefaults:

module MySpec = struct
  include SpecDefaults
  ...
end

This way new optional specs can be added as long as SpecDetaults can provide default implementations of such additions.

There is a PR to Picos that uses this PR.

TODO:

• Agree this is the way to go
• Document the API additions
• Finish the implementation, including creating STM_thread.MakeExt, and making sure operations are wrapped in all cases
• Update changelog

[jmid]

Thanks for this! 🙏

I've played a bit with it locally, rewriting existing STM tests to use it. This made me realize that both MakeExt and Make clients can use include SpecDefaults which is a net-win IMO - even for users just sticking to Make.
To ensure against regressions, I've also checked that this shouldn't cause error finding regressions, by rerunning the statistical tests.

I spotted locally that this would emit a compiler warning, but I believe you've fixed that in a recent (force) push.

Naming-wise I think

• SpecExt and MakeExt are reasonable for extended specs
• SpecDefaults is also fair - and also works well with the STM. quantification

My only reservation is about the wrap name. I don't think it describes well what is being wrapped.
Something like wrap_cmd_seq or wrap_cmds would be a bit more saying. I'm open to other suggestions - and not particularly eager about any of these two. The doc-string for (the binding-formerly-known-as) wrap should probably also describe a bit more what is being wrapped.

Otherwise, I'm OK with this 🙂 👍

[polytypic]

I decided to rename to wrap_cmd_seq, because wrap_cmds might give the impression of wrapping each and every command separately.

[jmid]

LGTM. I spotted a couple of minor documentation nits while proof-reading.

[jmid]

CI summary for 263ae96: all 34 workflows passed.
Merging...

[jmid]

CI summary for merge to main:

• gh-pages failed due to still using setup-ocaml@v2 - fixed in CI updates #513

Out of 35 workflows - 1 failed with a CI related error