Message-ID: <20151006081912.GA2681@nebuchadnezzar.informatik.uni-erlangen.de>
Date:	Tue, 6 Oct 2015 10:19:12 +0200
From:	Valentin Rothberg <valentinrothberg@...il.com>
To:	"Luis R. Rodriguez" <mcgrof@...e.com>
Cc:	"Luis R. Rodriguez" <mcgrof@...not-panic.com>, mmarek@...e.com,
	josh@...htriplett.org, jbottomley@...n.com, geert@...ux-m68k.org,
	pebolle@...cali.nl, herbert@...dor.apana.org.au, tiwai@...e.de,
	yann.morin.1998@...e.fr, corbet@....net,
	linux-kbuild@...r.kernel.org, linux-doc@...r.kernel.org,
	linux-kernel@...r.kernel.org, roberto@...osmo.org, zack@...ilon.cc,
	soos.mate@...il.com, skl@....ua.pt, iouliia@....ua.pt,
	Armin Biere <biere@....at>,
	Julia Lawall <julia.lawall@...6.fr>, ziegler@...fau.de
Subject: Re: [PATCH v3] kbuild: document recursive dependency limitation /
 resolution

On Oct 06 '15 01:03, Luis R. Rodriguez wrote:
> On Sun, Oct 04, 2015 at 03:42:47PM +0200, Valentin Rothberg wrote:
> > Hi Luis,
> > 
> > I finally found some time to read your patch.  Thanks for doing this
> > work in such great detail.
> > 
> > What I miss in the text is a general discussion of the widespread use of
> > selects.  In my opinion, selects should be (like gotos) considered
> > harmful:
> > 
> > First, selects ignore the user selection and all feature constraints:  a
> > symbol can be selected regardless if this breaks the constraints induced
> > by dependencies.  
> 
> Shouldn't such items not be selectable if the dependencies could not be met?

Yes and no :-)  Selects can be made conditional 'select FOO if BAR', to
restrict the targets to some condition.

> > Second, in my experience, selects are oftentimes used
> > to make manual configuration of the kernel easier, since a given symbol
> > is visible to the user even when the symbol's dependency is not yet
> > selected.
> 
> Sure, this is perhaps a good use case way to declare why select exists. I still
> think it would not be selectable unless the dependencies could be met ? If a
> select is enabling a config environement that would otherwise break dependencies
> it would seem to be a bug.

It's actually a feature, see Documentation/kbuild/kconfig-language.txt:

106   Note:                                                       
107     select should be used with care. select will force        
108     a symbol to a value without visiting the dependencies.    

Another use case of selects:
selects are also used to pre-select some core features such as PCI for
x86.  Using 'def_bool y' is sometimes not possible when multiple
archictectures share the same Kconfig file.

> > In contrast to a select, a symbol using a dependency is only
> > visible to the user when its dependency are satisfied.  I see it as a
> > decision between being semantically correct (depends) and being easy to
> > configure/user friendly (select).
> 
> Good point, something easy to configure should however still likely only
> be visible to the user if and only if it would not break existing user
> config. If we are not ensuring that now its perhaps good to annotate that
> as a desirable future feature.

I agree, it's a very desirable feature.  However, we need a SAT solver
for that :-)

> > The danger of using selects is already mentioned in the description of
> > selects, but I believe that it's good to raise awareness on top of what
> > you already wrote down.
> 
> Is that orthogonal to what my patch does? If not can you amend and I can
> integrate that into a v4? I seem to need to update some refrences to a
> SAT solver proposal so I think I need a v4 now.

I think that a general remark that using selects should be discouraged
as, besides causing the recursive issue, selects can also break
dependencies.

> > On Sep 23 '15 09:41, Luis R. Rodriguez wrote:
> > > From: "Luis R. Rodriguez" <mcgrof@...e.com>
> > > 
> > > Recursive dependency issues with kconfig are unavoidable due to
> > > some limitations with kconfig, since these issues are recurring
> > > provide a hint to the user how they can resolve these dependency
> > > issues and also document why such limitation exists.
> > > 
> > > While at it also document a bit of future prospects of ways to
> > > enhance Kconfig, including providing formal semantics and evaluation
> > > of use of a SAT solver.
> > > 
> > > Cc: Geert Uytterhoeven <geert@...ux-m68k.org>
> > > Cc: James Bottomley <jbottomley@...n.com>
> > > Cc: Josh Triplett <josh@...htriplett.org>
> > > Cc: Paul Bolle <pebolle@...cali.nl>
> > > Cc: Herbert Xu <herbert@...dor.apana.org.au>
> > > Cc: Takashi Iwai <tiwai@...e.de>
> > > Cc: "Yann E. MORIN" <yann.morin.1998@...e.fr>
> > > Cc: Michal Marek <mmarek@...e.com>
> > > Cc: Jonathan Corbet <corbet@....net>
> > > Cc: Mate Soos <soos.mate@...il.com>
> > > Cc: linux-kbuild@...r.kernel.org
> > > Cc: linux-doc@...r.kernel.org
> > > Cc: linux-kernel@...r.kernel.org
> > > Signed-off-by: Luis R. Rodriguez <mcgrof@...e.com>
> > > ---
> > > 
> > > This v3 builds up on requests on the v2 patch [0] by Josh first to clarify use
> > > of a SAT solver remains purely theoretical to address the known recursive
> > > dependency issues, and lastly then feedback by Paul to clarify why we
> > > have the recursive dependency issues. Since I still think the practical
> > > implications I was trying to clarify are important for developers to be
> > > aware of I've separated that into a different subsection. Lastly, I've added
> > > two subsections so that folks interested in advancing Kconfig can dig into
> > > to try to help address the feasibility of using a SAT solver with Kconfig.
> > > 
> > > I should also note that prospect use of SAT solvers on Linux is not only
> > > limited to Kconfig, however some areas may obviously require smaller time
> > > resolution constraints. For instance another theoretical area is in the use of
> > > kernel call site use of 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. Hardware assisted SAT solutions are known to exist
> > > but R&D for it is still in early stages [1] [2] [3].
> > > 
> > > [0] http://lkml.kernel.org/r/1438200556-13842-1-git-send-email-mcgrof@do-not-panic.com
> > > [1] https://dl.acm.org/citation.cfm?id=1025035
> > > [2] http://sweet.ua.pt/iouliia/Papers/2004/SSPA_FPL.pdf
> > > [3] http://link.springer.com/chapter/10.1007/978-3-540-71431-6_32
> > > 
> > >  Documentation/kbuild/Kconfig.recursion-issue-01 |  13 ++
> > >  Documentation/kbuild/Kconfig.recursion-issue-02 |  17 ++
> > >  Documentation/kbuild/kconfig-language.txt       | 233 ++++++++++++++++++++++++
> > >  scripts/kconfig/symbol.c                        |   2 +
> > >  4 files changed, 265 insertions(+)
> > >  create mode 100644 Documentation/kbuild/Kconfig.recursion-issue-01
> > >  create mode 100644 Documentation/kbuild/Kconfig.recursion-issue-02
> > > 
> > > diff --git a/Documentation/kbuild/Kconfig.recursion-issue-01 b/Documentation/kbuild/Kconfig.recursion-issue-01
> > > new file mode 100644
> > > index 000000000000..a097973025e7
> > > --- /dev/null
> > > +++ b/Documentation/kbuild/Kconfig.recursion-issue-01
> > > @@ -0,0 +1,13 @@
> > > +mainmenu "Simple example to demo kconfig recursive dependency issue"
> > > +
> > > +config CORE
> > > +	tristate
> > > +
> > > +config CORE_BELL_A
> > > +	tristate
> > > +	depends on CORE
> > > +
> > > +config CORE_BELL_A_ADVANCED
> > > +	tristate
> > > +	depends on CORE_BELL_A
> > > +	select CORE
> > > diff --git a/Documentation/kbuild/Kconfig.recursion-issue-02 b/Documentation/kbuild/Kconfig.recursion-issue-02
> > > new file mode 100644
> > > index 000000000000..b6282623336f
> > > --- /dev/null
> > > +++ b/Documentation/kbuild/Kconfig.recursion-issue-02
> > > @@ -0,0 +1,17 @@
> > > +mainmenu "Simple example to demo cumulative kconfig recursive dependency implication"
> > > +
> > > +config CORE
> > > +	tristate
> > > +
> > > +config CORE_BELL_A
> > > +	tristate
> > > +	depends on CORE
> > > +
> > > +config CORE_BELL_A_ADVANCED
> > > +	tristate
> > > +	select CORE_BELL_A
> > > +
> > > +config CORE_BELL_B
> > > +	tristate
> > > +	depends on !CORE_BELL_A
> > > +	select CORE
> > 
> > Switching between files to read one text can be confusing.  Hence, it
> > might be easier for a reader to understand the recursive issue when the
> > problem descriptions of both examples were placed in the corresponding
> > files.
> 
> Ah but we want users to use the file to run 'make menuconfig' on them.
> Or do you mean to stuff this text into the comment section of the Kconfig
> sample files?

Oh, sorry, I missed that.  Putting it into the comments section would be
nice then.

> > > diff --git a/Documentation/kbuild/kconfig-language.txt b/Documentation/kbuild/kconfig-language.txt
> > > index 350f733bf2c7..3b51d6b8c14f 100644
> > > --- a/Documentation/kbuild/kconfig-language.txt
> > > +++ b/Documentation/kbuild/kconfig-language.txt
> > > @@ -393,3 +393,236 @@ config FOO
> > >  	depends on BAR && m
> > >  
> > >  limits FOO to module (=m) or disabled (=n).
> > > +
> > > +Kconfig recursive dependency limitations
> > > +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> > > +
> > > +If you've hit the Kconfig error: "recursive dependency detected" you've run
> > > +into a recursive dependency issue with Kconfig. Kconfig does not do recursive
> > 
> > It seems like a good point here to define what you mean by ``recursive
> > dependency'', that's something I miss in the text.
> 
> I see, well its not defined until the next section in the simple example.
> In the section "Simple Kconfig recursive issue", so I can point to that.
> Unless of course we want to provide a summary of the issue as just a
> "circular" relationship. I think the reference may suffice to the section
> below?

Describing it as circular dependency and saying that Kconfig can't
resolve them would be fine for me.

> > > +dependency resolution; this has a few implications for Kconfig file writers.
> > > +We'll first explain why this issues exists and then provide an example
> > > +technical limitation which this brings upon Kconfig developers. Eager
> > > +developers wishing to try to address this limitation should read the
> > > +next subsection.
> > > +
> > > +The kconfig tools need to ensure that their input complies with the
> > > +configuration requirements specified in the various Kconfig files. In
> > > +order to do that they must determine the values that are possible for
> > > +all Kconfig symbols. And that is not possible if there is a circular
> > > +relation between two or more Kconfig symbols. We'll review the simplest
> >     
> >     ^ circular vs recursive ... I assume you mean the same thing
> 
> Indeed.
> 
> > > +type of recursive dependency issue with an example and explain why the
> > > +recursive dependency exists. Consider the example Kconfig file
> > > +Documentation/kbuild/Kconfig.recursion-issue-01, you can test it with.
> > > +
> > 
> > As written before, I prefer to have the problem descriptions /
> > explanations of both examples in their files.
> 
> It would have to go in as comments, is that OK format?

Awesome, thanks.

> >  Below, a more general
> > text would be nice:
> >     How does the problem look like?
> >     Why and how do such situations occur?
> >     How can the recursions be resolved?
> > 
> > Thereby, you could merge Simple and Cumulative and then jump to how they
> > can be fixed.
> 
> Not sure I follow what you are proposing  here.

When the descriptions of example 1 & 2 are moved to those files, you
somehow need to point to those files which can then be a more general
description of the problem.

> > > +Simple Kconfig recursive issue
> > > +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> > > +
> > > +Read: Documentation/kbuild/Kconfig.recursion-issue-01
> > > +
> > > +Test with:
> > > +
> > > +make KBUILD_KCONFIG=Documentation/kbuild/Kconfig.recursion-issue-01 allnoconfig
> > > +
> > > +This Kconfig file has a simple recursive dependency issue. In order to
> > > +understand why this recursive dependency issue occurs lets consider what
> > > +Kconfig needs to address. We iterate over what Kconfig needs to address
> > > +by stepping through the questions it needs to address sequentially.
> > > +
> > > + * What values are possible for CORE?
> > > +
> > > +CORE_BELL_A_ADVANCED selects CORE, which means that it influences the values
> > > +that are possible for CORE. So for example if CORE_BELL_A_ADVANCED is 'y',
> > > +CORE must be 'y' too.
> > > +
> > > + * What influences CORE_BELL_A_ADVANCED ?
> > > +
> > > +As the name implies CORE_BELL_A_ADVANCED is an advanced feature of CORE_BELL_A
> > > +so naturally it depends on CORE_BELL_A. So if CORE_BELL_A is 'y' we know
> > > +CORE_BELL_A_ADVANCED can be 'y' too.
> > > +
> > > +  * What influences CORE_BELL_A ?
> > > +
> > > +CORE_BELL_A depends on CORE, so CORE influences CORE_BELL_A.
> > > +
> > > +But that is a problem, because this means that in order to determine
> > > +what values are possible for CORE we ended up needing to address questions
> > > +regarding possible values of CORE itself again. Answering the original
> > > +question of what are the possible values of CORE would make the kconfig
> > > +tools run in a loop. When this happens Kconfig exits and complains about
> > > +the "recursive dependency detected" error.
> > > +
> > > +Reading the Documentation/kbuild/Kconfig.recursion-issue-01 file it may be
> > > +obvious that an easy to solution to this problem should just be the removal
> > > +of the "select CORE" from CORE_BELL_A_ADVANCED as that is implicit already
> > > +since CORE_BELL_A depends on CORE. Recursive dependency issues are not always
> > > +so trivial to resolve, we provide another example below of practical
> > > +implications of this recursive issue where the solution is perhaps not so
> > > +easy to understand. Note that matching semantics on the dependency on
> > > +CORE also consist of a solution to this recursive problem.
> > > +
> > > +Cumulative Kconfig recursive issue
> > > +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> > > +
> > > +Read: Documentation/kbuild/Kconfig.recursion-issue-02
> > > +
> > > +Test with:
> > > +
> > > +make KBUILD_KCONFIG=Documentation/kbuild/Kconfig.recursion-issue-02 allnoconfig
> > > +
> > > +The recursive limitations with Kconfig has some non intuitive implications
> > > +on kconfig sematics which are documented in this subsection. One known
> > > +practical implication of the recursive limitation is that drivers cannot
> > > +negate features from other drivers if they share a common core requirement and
> > > +use disjoint semantics to annotate those requirements, ie, some drivers use
> > > +"depends on" while others use "select". For instance it means if a driver A
> > > +and driver B share the same core requirement, and one uses "select" while the
> > > +other uses "depends on" to annotate this, all features that driver A selects
> > > +cannot now be negated by driver B.
> > > +
> > > +A perhaps not so obvious implication of this is that, if semantics on these
> > > +core requirements are not carefully synced, as drivers evolve features
> > > +they select or depend on end up becoming shared requirements which cannot be
> > > +negated by other drivers.
> > > +
> > > +The example provided in Documentation/kbuild/Kconfig.recursion-issue-02
> > > +describes a simple driver core layout of example features a kernel might
> > > +have. Let's assume we have some CORE functionality, then the kernel has a
> > > +series of bells and whistles it desires to implement, its not so advanced so
> > > +it only supports bells at this time: CORE_BELL_A and CORE_BELL_B. If
> > > +CORE_BELL_A has some advanced feature CORE_BELL_A_ADVANCED which selects
> > > +CORE_BELL_A then CORE_BELL_A ends up becoming a common BELL feature which
> > > +other bells in the system cannot negate. The reason for this issue is
> > > +due to the disjoint use of semantics on expressing each bell's relationship
> > > +with CORE, one uses "depends on" while the other uses "select".
> > > +
> > > +To fix this the "depends on CORE" must be changed to "select CORE", or the
> > > +"select CORE" must be changed to "depends on CORE".
> > > +
> > > +For an example real world scenario issue refer to the attempt to remove
> > > +"select FW_LOADER" [0], in the end the simple alternative solution to this
> > > +problem consisted on matching semantics with newly introduced features.
> > > +
> > > +[0] http://lkml.kernel.org/r/1432241149-8762-1-git-send-email-mcgrof@do-not-panic.com
> > > +
> > > +Practical solutions to kconfig recursive issue
> > > +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> > > +
> > > +Developers who run into the recursive Kconfig issue have three options
> > > +at their disposal. We document them below and also provide a list of
> > > +historical issues resolved through these different solutions.
> > > +
> > > +  a) Remove any superfluous "select FOO" or "depends on FOO"
> > > +  b) Match dependency semantics:
> > > +	b1) Swap all "select FOO" to "depends on FOO" or,
> > > +	b2) Swap all "depends on FOO" to "select FOO"
> > > +
> > > +The resolution to a) can be tested with the sample Kconfig file
> > > +Documentation/kbuild/Kconfig.recursion-issue-01 through the removal
> > > +of the "select CORE" from CORE_BELL_A_ADVANCED as that is implicit already
> > > +since CORE_BELL_A depends on CORE. At times it may not be possible to remove
> > > +some dependency criteria, for such cases you can work with solution b).
> > > +
> > > +The two different resolutions for b) can be tested in the sample Kconfig file
> > > +Documentation/kbuild/Kconfig.recursion-issue-02.
> > > +
> > > +Below is a list of examples of prior fixes for these types of recursive issues;
> > > +all errors appear to involve one or more select's and one or more "depends on".
> > > +
> > > +commit          fix
> > > +======          ===
> > > +06b718c01208    select A -> depends on A
> > > +c22eacfe82f9    depends on A -> depends on B
> > > +6a91e854442c    select A -> depends on A
> > > +118c565a8f2e    select A -> select B
> > > +f004e5594705    select A -> depends on A
> > > +c7861f37b4c6    depends on A -> (null)
> > > +80c69915e5fb    select A -> (null)              (1)
> > > +c2218e26c0d0    select A -> depends on A        (1)
> > > +d6ae99d04e1c    select A -> depends on A
> > > +95ca19cf8cbf    select A -> depends on A
> > > +8f057d7bca54    depends on A -> (null)
> > > +8f057d7bca54    depends on A -> select A
> > > +a0701f04846e    select A -> depends on A
> > > +0c8b92f7f259    depends on A -> (null)
> > > +e4e9e0540928    select A -> depends on A        (2)
> > > +7453ea886e87    depends on A > (null)           (1)
> > > +7b1fff7e4fdf    select A -> depends on A
> > > +86c747d2a4f0    select A -> depends on A
> > > +d9f9ab51e55e    select A -> depends on A
> > > +0c51a4d8abd6    depends on A -> select A        (3)
> > > +e98062ed6dc4    select A -> depends on A        (3)
> > > +91e5d284a7f1    select A -> (null)
> > > +
> > > +(1) Partial (or no) quote of error.
> > > +(2) That seems to be the gist of that fix.
> > > +(3) Same error.
> > 
> > ^ It's awesome to have list like above.
> 
> That was thanks to Paul.

Thanks Paul :-)

> > > +
> > > +Future kconfig work
> > > +~~~~~~~~~~~~~~~~~~~
> > > +
> > > +Work on kconfig is welcomed on both areas of clarifying semantics and on
> > > +evaluating the use of a full SAT solver for it. A full SAT solver can be
> > > +desirable to enable more complex dependency mappings and / or queries,
> > > +for instance on possible use case for a SAT solver could be that of handling
> > > +the current known recursive dependency issues. It is not known if this would
> > > +address such issues but such evaluation is desirable. If support for a full SAT
> > > +solver proves too complex or that it cannot address recursive dependency issues
> > > +Kconfig should have at least clear and well defined semantics which also
> > > +addresses and documents limitations or requirements such as the ones dealing
> > > +with recursive dependencies.
> > > +
> > > +Further work on both of these areas is welcomed on Kconfig. We elaborate
> > > +on both of these in the next two subsections.
> > > +
> > > +Semantics of Kconfig
> > > +~~~~~~~~~~~~~~~~~~~~
> > > +
> > > +The use of Kconfig is broad, Linux is now only one of Kconfig's users:
> > > +one study has completed a broad analysis of Kconfig use in 12 projects [0].
> > > +Despite its widespread use, and although this document does a reasonable job
> > > +in documenting basic Kconfig syntax a more precise definition of Kconfig
> > > +semantics is welcomed. One project deduced Kconfig semantics through
> > > +the use of the xconfig configurator [1]. Work should be done to confirm if
> > > +the deduced semantics matches our intended Kconfig design goals.
> > > +
> > > +Having well defined semantics can be useful for tools for practical
> > > +evaluation of depenencies, for instance one such use known case was work to
> > > +express in boolean abstraction of the inferred semantics of Kconfig to
> > > +translate Kconfig logic into boolean formulas and run a SAT solver on this to
> > > +find dead code / features (always inactive), 114 dead features were found in
> > > +Linux using this methodology [1] (Section 8: Threats to validity).
> > > +
> > > +Confirming this could prove useful as Kconfig stands as one of the the leading
> > > +industrial variability modeling languages [1] [2]. Its study would help
> > > +evaluate practical uses of such languages, their use was only theoretical
> > > +and real world requirements were not well understood. As it stands though
> > > +only reverse engineering techniques have been used to deduce semantics from
> > > +variability modeling languages such as Kconfig [3].
> > > +
> > > +[0] http://www.eng.uwaterloo.ca/~shshe/kconfig_semantics.pdf
> > > +[1] http://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf
> > > +[2] http://gsd.uwaterloo.ca/sites/default/files/ase241-berger_0.pdf
> > > +[3] http://gsd.uwaterloo.ca/sites/default/files/icse2011.pdf
> > 
> > A highly related project is CADOS [1] (former VAMOS [2]) and the tools,
> > mainly undertaker [3], which has been introduced first with [4].  The
> > basic concept of undertaker is to exract variability models from
> > Kconfig, and put them together with a propositional formula extracted
> > from CPP #ifdefs and build-rules into a SAT solver in order to find dead
> > code, dead files, and dead symbols.
> > 
> > [1] https://cados.cs.fau.de
> > [2] https://vamos.cs.fau.de
> > [3] https://undertaker.cs.fau.de
> > [4] https://www4.cs.fau.de/Publications/2011/tartler_11_eurosys.pdf
> 
> Thanks, I'll stuff that in.
> 
> > > +Full SAT solver for Kconfig
> > > +~~~~~~~~~~~~~~~~~~~~~~~~~~~
> > > +
> > > +Although SAT solvers [0] haven't yet been used by Kconfig directly, as noted in
> > > +the previous subsection, work has been done however to express in boolean
> > > +abstraction the inferred semantics of Kconfig to translate Kconfig logic into
> > > +boolean formulas and run a SAT solver on it [1]. If using a SAT solver is
> > > +desirable on Kconfig one approach would be to evaluate repurposing such effort
> > > +somehow on Kconfig. The 3-year Mancoosi research project [1] challenged
> > > +researchers and developers with solutions for software package resolution
> > > +dependencies requiring free software licenses for proposed solutions, some of
> > > +the solutions proposed used SAT solvers, one of which was CryManSolver which
> > > +used CryptoMiniSat [3] [4] as backend (a SAT solver in itself). CryptoMiniSat
> > > +remains of the only SAT solvers which aims to be fully open that also has a
> > > +relatively clean C++ / Python interface. Evaluation of CryptoMiniSat for use
> > > +with Kconfig is desirable.
> > > +
> > > +[0] http://www.cs.cornell.edu/~sabhar/chapters/SATSolvers-KR-Handbook.pdf
> > > +[1] http://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf
> > > +[2] http://mancoosi.org/
> > > +[3] http://www.msoos.org/cryptominisat4/
> > > +[4] https://github.com/msoos/cryptominisat/
> > 
> > As mentioned in a different mail thread, undertaker uses PicoSAT [5].  I
> > am no expert in SAT solving, but PicoSAT works reliably fast, it is
> > written in C and also ships PicoMUS to generate a Minimally
> > Unsatisfiable Subformula.  We use it the MUS to understand which Kconfig
> > symbols contribute to a boolean contradiction when analyzing dead
> > features or dead code, etc.  It is a powerful tool and could be
> > interesting especially in the context of Kconfig.
> > 
> > Hence, I suggest to add [5] to list above to consider it in future
> > evaluations.
> > 
> > [5] http://fmv.jku.at/picosat/
> 
> Indeed. Will do, and fortunately Armin considers this as sensible and seems
> willing to help maintain such code if we end up using it on Linux. Since I
> don't have time and this seems to be a generally self contained effort I think
> this might be a very nicely suited project for Outreachy. I'd be up to help
> mentor this work. If anyone else is please let me know.
> 
> Unless of course someone tells me now that they're interested in doing this work
> right away :)
> 
>   Luis
--
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@...r.kernel.org
More majordomo info at  http://vger.kernel.org/majordomo-info.html
Please read the FAQ at  http://www.tux.org/lkml/

Powered by blists - more mailing lists