= 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