= Linux SAT integration =

SAT solver technology has been advancing steadily over the last few years.
A lot of these advancements can be explained by a series of competitions
held in different areas which have not only spurred interest into the field
but also concrete solutions. The state of the art of SAT solvers is now even
shifting into hardware space, but yet remains part of ongoing research.

This page is intended to document areas of interest where a SAT solver
could potentially be used on Linux, both in software or perhaps in the
future with hardware assisted SAT solving solutions.

[[TableOfContents(4)]]

= Kconfig =

The first taste of a SAT solver in Linux the kernel could be with
integration and use of Kconfig. The interest and work for that is
being documented separately on the [http://kernelnewbies.org/KernelProjects/kconfig-sat kconfig-sat]
project page.

= Sorting functional dependencies between devices =

SAT solvers have been known to help with ordering package dependency problems, helping improve the not
only if a request is satisfiable but also help with the most optimal solution. A SAT solver could
potentially be used to help with optimizing asynchronous boot and device dependency management.

Sometimes Linux cannot annotate dependencies between devices though. This can cause a few problems
or means having to implement hacks on the kernel. One known hack is the use of deferred probe,
returning -EPROBE_DEFER on probe as a requirement is determined to not yet be available. Another
is not being sure one can do suspend and resume in the right order. We need both semantics to
address these shortcomings but also a way to figure out the optimal dependency order needed.

== Defining functional dependency ==

  "A is functionally dependent on on B"

Functional dependency is defined as a requirement of driver B needing both
device and driver A to be functional and present in order to work.  This implies that the
driver of A needs to be working for B to be probed successfully.

=== Linux deferred probe ===

When Linux boots some drivers currently return -EPROBE_DEFER on their device driver probe routine,
this tells the driver core to put the device driver into a linked list on init and try re-probing later.
The driver may use -EPROBE_DEFER as it may have not yet found a requirement present up yet. The
driver does this as *sometimes* the kernel doesn't have dependency information available, or there
is no way to currently annotate this. As an example an SDHCI driver may first need a GPIO line from
an i2c GPIO controller before it can be initialized.

From a power management perspective A being functional dependent on B means driver A cannot be
unbound from the device before the B's driver.

=== Linux suspend / resume ===

From a power management perspective A being functional dependent on B means that for suspend
driver B to needs to wait for driver A to suspend. For resume it means driver A needs to wait 
for driver B to resume.

=== Current proposed solutions ===

Rafael J. Wysocki described the functional dependency problem 
[https://lwn.net/Articles/671858/ best recently] and also proposed a new mechanism to annotate
functional relationship between devices. As Rafael proposes, each device driver can claim a
possible set of consumers it can help or a set of suppliers it needs.

In Rafael's proposal there is the concept of two types of links. A permanent link and a
probe time link. A permanent link will stay around until one of the linked devices is
unregistered, at which time the driver core will drop the link along with the device
going away. A probe-time link will be dropped (automatically) at the consumer device
driver unbind time.

This is not yet upstream.

=== What a solution means ===

A proper solution to this problem should not only help avoid using -EPROBE_DEFER but also help
with enabling better ordering for suspend and resume. While we don't have a count for
for device drivers needing a solution from a power management perspective as it stands
we have well over ~500 uses of -EPROBE_DEFER on device drivers.

To help with this we need both semantics to help annotate functional dependencies between
different subsystems and a way to help the kernel sort these.

Once a formal solution on dependency annotation is found both at device probe and
suspend/resume, devices depending on others can wait until its suppliers are
made available. The ordering will happen asynchronously at first though. A SAT
solver might help with analysis of the dependency graph and help with ordering
and optimize boot time by ordering device ordering as best as possible.

= Linux scheduler =

One area could be in select_idle_sibling() where the schedular checks if the
overall compute and NUMA accesses of the system would be improved if the source
tasks were migrated to another target CPU. Such use would require a resolution
in the thousands of CPU cycles time frame, and the size of the problems will
vary depending on the number of CPUs, topology, and workloads.

In addition workload parameters in particular can vary extremely fast, its not
even certain yet if these problems can be represented as a SAT problem at the moment.

Another optimization consideration would be the requirement for scheduling
decisions to have all data locally avaiable, offloading such problems would
very likely not be viable solution, for instance, so fully hardware assisted
SAT solvers '''may be required'''.

= Review of state of the art on hardware assisted SAT solvers =

Hardware assisted SAT solutions are known to exist but R&D for it is still in early stages:

  * https://dl.acm.org/citation.cfm?id=1025035
  * http://sweet.ua.pt/iouliia/Papers/2004/SSPA_FPL.pdf
  * http://link.springer.com/chapter/10.1007/978-3-540-71431-6_32