Draft: specification for concurrency support in IPASIR2

[fkutzner]

Problem

The original IPASIR API (biotomas/ipasir@de0ac2b, SAT Race 2015 publication) does not specify any thread safety requirements. This should be fixed in IPASIR2. For clients, I think the most relevant use case is to be able to set up and run solvers in parallel, but they don't need to be able to call functions in parallel on the same solver object (callback functions complicate this a bit, see below).

For example, the genipafolio example application uses IPASIR solvers in parallel.

Proposal

The following is just a rough idea (2023-08-22, currently for a55e413, work in progress).

Assumptions:

• No extra complexity should be introduced for single-threaded IPASIR2 solvers.
• Commonly, clients assume IPASIR2 solvers to be (or, at least, to behave like) single-threaded solvers, so clients should not be forced to implement synchronization in their callback functions.
• For clients that explicitly support it, multithreaded solvers should be able to invoke the callback functions in parallel.

Proposal:

1. Concurrent calls of IPASIR2 functions are allowed, but only for different solver instances (ie. different first arguments). Exceptions:
   1.1 ...for functions without solver arguments: ipasir2_init(), ipasir2_signature(), ipasir2_options() may always be called, even in parallel.
   1.2 ...for ipasir2_solve: during the execution a callback via ipasir2_solve(), the client may call any function on the calling solver object which is allowed in the SOLVING state, but at most one at a time from each callback execution.
2. An IPASIR2 solver instance may not call any callback functions provided to it by the client in parallel, unless the client allows this by setting a corresponding option before invoking ipasir_solve() (default: not allowed). However, solver instances may invoke callback functions independently from other IPASIR2 solvers running at the same time.

Remarks

• For single-threaded solver implementations, the requirements are trivial to meet.
• No synchronization is needed between solver instances.
• By default, clients can expect that callbacks aren't invoked in parallel by a given solver instance - not even different callbacks.
• During ipasir2_solve(), clients can call functions allowed during the SOLVING state only while a callback passed to the solver is running.
• There is no requirement that the callbacks are called from the same thread in which ipasir2_solve was called.

TODOs & open questions:

• Should IPASIR2 define a concurrency-related option? As a first step, we could specify the default behavior but allow implementations to override it via options. We could add a common option later, if needed.
• The lifetime requirements for clauses returned from callbacks need to be adjusted for the multithreaded case - for example, if clients allow it, solvers may invoke the import callback from multiple threads. This remains to be addressed. The lifetime requirement for clauses returned from the import callback is awkward for clients anyway - maybe we could revisit that [added 2023-08-22]

[Udopia]

Nice addition to the specification. I particularly like to the part which specifies that clients can actually rely on non-overlapping callback invocations.

[fkutzner]

I think we could eliminate the lifetime problem entirely by not returning clauses from the import callback, but allow ipasir2_add to be called while solving (but then, only from the import callback). This would require revamping the ipasir2_add function a bit - it would need an ipasir2_redundancy parameter and should also take a clause instead of individual literals. I think this is a good case for changing ipasir2_add anyway, because with this approach, clients don't have to keep the most recently imported clause around after the import callback finishes.

This shouldn't be too hard to do for IPASIR2 implementations - they could just wrap the callback, or they could copy clauses added during ipasir2_solve into a buffer provided by the solver.

What do you think?

[Udopia]

Having not the import-callback return the clause, but allowing ipasir2_add to be called from the callback solves the scoping issue in a nice way. Otherwise, we need a specification like the following: "the clause must exist either until the next call to import or until the end of solve".

With your suggestion, the imported clause can be freed right after the call to ipasir2_add. Adding the ipasir2_redundancy parameter to ipasir2_add has additional nice side-effects for applications generating redundant clauses in a preprocessing step, e.g. BVA or SBP, can mark them as such.

If we change the signature of ipasir2_add anyways, then I would also be more inclined to change to a buffer+length representation in the same move.

[Udopia]

I just adapted the signature of the import callback to reflect the changes announced above: ipasir2_set_import

Now ipasir2_add can be used by the callback in SOLVING state and has one additional parameter to indicate the redundancy type.

We now need to think better about specifying redundancy types. It used to be easier to specify the formula F with respect to which the imported clauses must have a particular redundancy property, because then F was simply the formula added by ipasir2_add. Now, since the import also runs through ipasir2_add, we could either make a distinction based on the INPUT and SOLVING states in which add() was called, or simply refer to all added clauses before the current solve() call. I consider the latter to be the simplest solution, and think that it is sufficient and unproblematic.