[PATCH] kbuild: document recursive dependency limitation / resolution

[PATCH] kbuild: document recursive dependency limitation / resolution

[Luis R. Rodriguez]

From: "Luis R. Rodriguez" <mcgrof@suse.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.

Cc: Geert Uytterhoeven <geert@linux-m68k.org>
Cc: James Bottomley <jbottomley@odin.com>
Cc: Josh Triplett <josh@joshtriplett.org>
Cc: Paul Bolle <pebolle@tiscali.nl>
Cc: Herbert Xu <herbert@gondor.apana.org.au>
Cc: Takashi Iwai <tiwai@suse.de>
Cc: "Yann E. MORIN" <yann.morin.1998@free.fr>
Cc: Michal Marek <mmarek@suse.com>
Cc: Jonathan Corbet <corbet@lwn.net>
Cc: linux-kbuild@vger.kernel.org
Cc: linux-doc@vger.kernel.org
Cc: linux-kernel@vger.kernel.org
Signed-off-by: Luis R. Rodriguez <mcgrof@suse.com>
---

I've cc'd Roberto and Stefano as I think we might be able to in the
long term use some of their work on package dependency and solvers for
this problem [0] [1] [2]. This last part -- just consider it long term
focused.

[0] https://upsilon.cc/~zack/research/publications/splc2010-fd-deps.pdf
[1] https://ocaml.org/meetings/ocaml/2014/preferences-2014-09-05-slides.pdf
[2] https://www.youtube.com/watch?v=GSOcRQvZg8w

 Documentation/kbuild/kconfig-language.txt | 22 ++++++++++++++++++++++
 scripts/kconfig/symbol.c                  |  2 ++
 2 files changed, 24 insertions(+)

diff --git a/Documentation/kbuild/kconfig-language.txt b/Documentation/kbuild/kconfig-language.txt
index 350f733bf2c7..7e0510d1cef7 100644
--- a/Documentation/kbuild/kconfig-language.txt
+++ b/Documentation/kbuild/kconfig-language.txt
@@ -393,3 +393,25 @@ 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
+dependency resolution, this has a few implications for Kconfig file writers. In
+practice it means that for instance if a driver A selects a few kconfig symbols
+another driver B which selects any of these symbols cannot negate any of the
+symbols the driver A selected.  Because of this current limitation developers
+who run into this type of recursive dependency issue have two diverging
+options:
+
+  a) Either swap all "select FOO" to "depends on FOO" or,
+  b) Change the offending "depends on FOO" to "select FOO"
+
+Kconfig's limitations can be addressed by implementing a SAT solver for it,
+but until then, Kconfig is limitted to require developers to use one of
+the above two mechanisms to address recursive dependency issues. For more
+details you can refer to this thread and discussion:
+
+http://lkml.kernel.org/r/1432241149-8762-1-git-send-email-mcgrof@do-not-panic.com
diff --git a/scripts/kconfig/symbol.c b/scripts/kconfig/symbol.c
index 70c5ee189dce..4d61b7490dad 100644
--- a/scripts/kconfig/symbol.c
+++ b/scripts/kconfig/symbol.c
@@ -1117,6 +1117,8 @@ static void sym_check_print_recursive(struct symbol *last_sym)
 		if (stack->sym == last_sym)
 			fprintf(stderr, "%s:%d:error: recursive dependency detected!\n",
 				prop->file->name, prop->lineno);
+			fprintf(stderr, "For a resolution refer to Documentation/kbuild/kconfig-language.txt\n");
+			fprintf(stderr, "section \"Kconfig recursive dependency limitations\"\n");
 		if (stack->expr) {
 			fprintf(stderr, "%s:%d:\tsymbol %s %s value contains %s\n",
 				prop->file->name, prop->lineno,
-- 
2.3.2.209.gd67f9d5.dirty

Re: [PATCH] kbuild: document recursive dependency limitation / resolution

[Randy Dunlap]

On 07/29/15 13:09, Luis R. Rodriguez wrote:
> From: "Luis R. Rodriguez" <mcgrof@suse.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.
> 
> Cc: Geert Uytterhoeven <geert@linux-m68k.org>
> Cc: James Bottomley <jbottomley@odin.com>
> Cc: Josh Triplett <josh@joshtriplett.org>
> Cc: Paul Bolle <pebolle@tiscali.nl>
> Cc: Herbert Xu <herbert@gondor.apana.org.au>
> Cc: Takashi Iwai <tiwai@suse.de>
> Cc: "Yann E. MORIN" <yann.morin.1998@free.fr>
> Cc: Michal Marek <mmarek@suse.com>
> Cc: Jonathan Corbet <corbet@lwn.net>
> Cc: linux-kbuild@vger.kernel.org
> Cc: linux-doc@vger.kernel.org
> Cc: linux-kernel@vger.kernel.org
> Signed-off-by: Luis R. Rodriguez <mcgrof@suse.com>
> ---
> 
> I've cc'd Roberto and Stefano as I think we might be able to in the
> long term use some of their work on package dependency and solvers for
> this problem [0] [1] [2]. This last part -- just consider it long term
> focused.
> 
> [0] https://upsilon.cc/~zack/research/publications/splc2010-fd-deps.pdf
> [1] https://ocaml.org/meetings/ocaml/2014/preferences-2014-09-05-slides.pdf
> [2] https://www.youtube.com/watch?v=GSOcRQvZg8w
> 
>  Documentation/kbuild/kconfig-language.txt | 22 ++++++++++++++++++++++
>  scripts/kconfig/symbol.c                  |  2 ++
>  2 files changed, 24 insertions(+)
> 
> diff --git a/Documentation/kbuild/kconfig-language.txt b/Documentation/kbuild/kconfig-language.txt
> index 350f733bf2c7..7e0510d1cef7 100644
> --- a/Documentation/kbuild/kconfig-language.txt
> +++ b/Documentation/kbuild/kconfig-language.txt
> @@ -393,3 +393,25 @@ 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
> +dependency resolution, this has a few implications for Kconfig file writers. In

maybe                 s/,/;/

> +practice it means that for instance if a driver A selects a few kconfig symbols
> +another driver B which selects any of these symbols cannot negate any of the
> +symbols the driver A selected.  Because of this current limitation developers
> +who run into this type of recursive dependency issue have two diverging
> +options:
> +
> +  a) Either swap all "select FOO" to "depends on FOO" or,
> +  b) Change the offending "depends on FOO" to "select FOO"
> +
> +Kconfig's limitations can be addressed by implementing a SAT solver for it,
> +but until then, Kconfig is limitted to require developers to use one of

                              limited

> +the above two mechanisms to address recursive dependency issues. For more
> +details you can refer to this thread and discussion:
> +
> +http://lkml.kernel.org/r/1432241149-8762-1-git-send-email-mcgrof@do-not-panic.com


-- 
~Randy

Re: [PATCH] kbuild: document recursive dependency limitation / resolution

[Michal Marek]

Dne 29.7.2015 v 22:34 Randy Dunlap napsal(a):
> On 07/29/15 13:09, Luis R. Rodriguez wrote:
>> From: "Luis R. Rodriguez" <mcgrof@suse.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.

Good idea.


>> +Kconfig's limitations can be addressed by implementing a SAT solver for it,
>> +but until then, Kconfig is limitted to require developers to use one of
> 
>                               limited

should I apply the patch with the typo fixed or are you going to send a v2?

Thanks,
Michal

Re: [PATCH] kbuild: document recursive dependency limitation / resolution

[Paul Bolle]

On di, 2015-08-04 at 13:57 +0200, Michal Marek wrote:
> should I apply the patch with the typo fixed or are you going to send 
> a v2?

I'm afraid I have been thinking about some comments for quite a few days
now. So a v2 would be appreciated.

Or, alternatively, Michal could perhaps wait another day and I promise
to actually make those comments. Is that OK?

Thanks either way,


Paul Bolle

Re: [PATCH] kbuild: document recursive dependency limitation / resolution

[Luis R. Rodriguez]

On Tue, Aug 04, 2015 at 01:57:21PM +0200, Michal Marek wrote:
> Dne 29.7.2015 v 22:34 Randy Dunlap napsal(a):
> > On 07/29/15 13:09, Luis R. Rodriguez wrote:
> >> From: "Luis R. Rodriguez" <mcgrof@suse.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.
> 
> Good idea.

Great I've expanded a bit on the future required work to feed the curious
so that we don't idle lingering what to do next but rather get folks engaged
and so that they can know where to dive in.

> 
> >> +Kconfig's limitations can be addressed by implementing a SAT solver for it,
> >> +but until then, Kconfig is limitted to require developers to use one of
> > 
> >                               limited
> 
> should I apply the patch with the typo fixed or are you going to send a v2?

I'll respin a v3 now.

  Luis

Re: [PATCH] kbuild: document recursive dependency limitation / resolution

[Luis R. Rodriguez]

On Wed, Jul 29, 2015 at 01:34:50PM -0700, Randy Dunlap wrote:
> On 07/29/15 13:09, Luis R. Rodriguez wrote:
> > +
> > +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
> > +dependency resolution, this has a few implications for Kconfig file writers. In
> 
> maybe                 s/,/;/

Fixed.

> > +practice it means that for instance if a driver A selects a few kconfig symbols
> > +another driver B which selects any of these symbols cannot negate any of the
> > +symbols the driver A selected.  Because of this current limitation developers
> > +who run into this type of recursive dependency issue have two diverging
> > +options:
> > +
> > +  a) Either swap all "select FOO" to "depends on FOO" or,
> > +  b) Change the offending "depends on FOO" to "select FOO"
> > +
> > +Kconfig's limitations can be addressed by implementing a SAT solver for it,
> > +but until then, Kconfig is limitted to require developers to use one of
> 
>                               limited
> 

I've re-written this section, thanks for the review.

  Luis

Re: [PATCH] kbuild: document recursive dependency limitation / resolution

[josh]

On Wed, Jul 29, 2015 at 01:09:16PM -0700, Luis R. Rodriguez wrote:
> From: "Luis R. Rodriguez" <mcgrof@suse.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.
> 
> Cc: Geert Uytterhoeven <geert@linux-m68k.org>
> Cc: James Bottomley <jbottomley@odin.com>
> Cc: Josh Triplett <josh@joshtriplett.org>
> Cc: Paul Bolle <pebolle@tiscali.nl>
> Cc: Herbert Xu <herbert@gondor.apana.org.au>
> Cc: Takashi Iwai <tiwai@suse.de>
> Cc: "Yann E. MORIN" <yann.morin.1998@free.fr>
> Cc: Michal Marek <mmarek@suse.com>
> Cc: Jonathan Corbet <corbet@lwn.net>
> Cc: linux-kbuild@vger.kernel.org
> Cc: linux-doc@vger.kernel.org
> Cc: linux-kernel@vger.kernel.org
> Signed-off-by: Luis R. Rodriguez <mcgrof@suse.com>

As a minor nit, I would suggest saying that making Kbuild handle this
might require a full SAT solver, rather than the current phrasing that
suggests that a SAT solver is the right solution to this problem.  Let's
wait to make that conclusion until a kbuild patch shows up.

Otherwise, this seems quite sensible; thanks for documenting this bit of
tribal knowledge.

- Josh Triplett

> I've cc'd Roberto and Stefano as I think we might be able to in the
> long term use some of their work on package dependency and solvers for
> this problem [0] [1] [2]. This last part -- just consider it long term
> focused.
> 
> [0] https://upsilon.cc/~zack/research/publications/splc2010-fd-deps.pdf
> [1] https://ocaml.org/meetings/ocaml/2014/preferences-2014-09-05-slides.pdf
> [2] https://www.youtube.com/watch?v=GSOcRQvZg8w
> 
>  Documentation/kbuild/kconfig-language.txt | 22 ++++++++++++++++++++++
>  scripts/kconfig/symbol.c                  |  2 ++
>  2 files changed, 24 insertions(+)
> 
> diff --git a/Documentation/kbuild/kconfig-language.txt b/Documentation/kbuild/kconfig-language.txt
> index 350f733bf2c7..7e0510d1cef7 100644
> --- a/Documentation/kbuild/kconfig-language.txt
> +++ b/Documentation/kbuild/kconfig-language.txt
> @@ -393,3 +393,25 @@ 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
> +dependency resolution, this has a few implications for Kconfig file writers. In
> +practice it means that for instance if a driver A selects a few kconfig symbols
> +another driver B which selects any of these symbols cannot negate any of the
> +symbols the driver A selected.  Because of this current limitation developers
> +who run into this type of recursive dependency issue have two diverging
> +options:
> +
> +  a) Either swap all "select FOO" to "depends on FOO" or,
> +  b) Change the offending "depends on FOO" to "select FOO"
> +
> +Kconfig's limitations can be addressed by implementing a SAT solver for it,
> +but until then, Kconfig is limitted to require developers to use one of
> +the above two mechanisms to address recursive dependency issues. For more
> +details you can refer to this thread and discussion:
> +
> +http://lkml.kernel.org/r/1432241149-8762-1-git-send-email-mcgrof@do-not-panic.com
> diff --git a/scripts/kconfig/symbol.c b/scripts/kconfig/symbol.c
> index 70c5ee189dce..4d61b7490dad 100644
> --- a/scripts/kconfig/symbol.c
> +++ b/scripts/kconfig/symbol.c
> @@ -1117,6 +1117,8 @@ static void sym_check_print_recursive(struct symbol *last_sym)
>  		if (stack->sym == last_sym)
>  			fprintf(stderr, "%s:%d:error: recursive dependency detected!\n",
>  				prop->file->name, prop->lineno);
> +			fprintf(stderr, "For a resolution refer to Documentation/kbuild/kconfig-language.txt\n");
> +			fprintf(stderr, "section \"Kconfig recursive dependency limitations\"\n");
>  		if (stack->expr) {
>  			fprintf(stderr, "%s:%d:\tsymbol %s %s value contains %s\n",
>  				prop->file->name, prop->lineno,
> -- 
> 2.3.2.209.gd67f9d5.dirty
> 

Re: [PATCH] kbuild: document recursive dependency limitation / resolution

[Luis R. Rodriguez]

On Wed, Jul 29, 2015 at 01:54:07PM -0700, josh@joshtriplett.org wrote:
> On Wed, Jul 29, 2015 at 01:09:16PM -0700, Luis R. Rodriguez wrote:
> > From: "Luis R. Rodriguez" <mcgrof@suse.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.
> > 
> > Cc: Geert Uytterhoeven <geert@linux-m68k.org>
> > Cc: James Bottomley <jbottomley@odin.com>
> > Cc: Josh Triplett <josh@joshtriplett.org>
> > Cc: Paul Bolle <pebolle@tiscali.nl>
> > Cc: Herbert Xu <herbert@gondor.apana.org.au>
> > Cc: Takashi Iwai <tiwai@suse.de>
> > Cc: "Yann E. MORIN" <yann.morin.1998@free.fr>
> > Cc: Michal Marek <mmarek@suse.com>
> > Cc: Jonathan Corbet <corbet@lwn.net>
> > Cc: linux-kbuild@vger.kernel.org
> > Cc: linux-doc@vger.kernel.org
> > Cc: linux-kernel@vger.kernel.org
> > Signed-off-by: Luis R. Rodriguez <mcgrof@suse.com>
> 
> As a minor nit, I would suggest saying that making Kbuild handle this
> might require a full SAT solver, rather than the current phrasing that
> suggests that a SAT solver is the right solution to this problem.  Let's
> wait to make that conclusion until a kbuild patch shows up.

Thanks I've clarified this some more and expanding completely on the
section on SAT solver with some references for the eager beavers. I have
also found some other use cases for SAT solver on Linux but since that
is out of the scope of Kconfig I'll leave it outside of the patch but after
the commit log so even more eager beavers can take action.

> Otherwise, this seems quite sensible; thanks for documenting this bit of
> tribal knowledge.

Thanks, I'll respin finally.

  Luis

Re: [PATCH] kbuild: document recursive dependency limitation / resolution

[Paul Bolle]

[Once again I removed Yann from the addresses used. I suppose I'll just
send a trivial patch to remove Yann's M: line for MAINTAINERS.]

Hi Luis,

On wo, 2015-07-29 at 13:09 -0700, Luis R. Rodriguez wrote:
> 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.
> 
> Signed-off-by: Luis R. Rodriguez <mcgrof@suse.com>

Like Josh and Marek I find this a good idea. Because I like the idea
I'll be critical.

> --- a/Documentation/kbuild/kconfig-language.txt
> +++ b/Documentation/kbuild/kconfig-language.txt
> @@ -393,3 +393,25 @@ 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
> +dependency resolution,

(True. But what could Kconfig do other than note that a chain of
select's and depend on's makes it run in circles? See below.)

>  this has a few implications for Kconfig file writers. In
> +practice it means that for instance if a driver A selects a few kconfig symbols
> +another driver B which selects any of these symbols cannot negate any of the
> +symbols the driver A selected.

I'm afraid I don't follow this.

> Because of this current limitation developers
> +who run into this type of recursive dependency issue have two diverging
> +options:
> +
> +  a) Either swap all "select FOO" to "depends on FOO" or,

all? "one or more" perhaps.

> +  b) Change the offending "depends on FOO" to "select FOO"

"the offending"? We're looking at a circle. So maybe:
    Change one or more "depends on BAR" to "select BAR"   

Which are both variations on a theme: stop running in circles. See below
for a (too?) small sample of 22 solutions I could easily find in git's
log. Swapping one or more select's with depend on's was done in two
thirds of these solutions.

> +Kconfig's limitations can be addressed by implementing a SAT solver for it,

Unlike Josh, I'm not familiar with SAT solvers, so it's hard to comment
on this.

But given the two building blocks involved:
    depends on
    select

it's clear you can make Kconfig run in circles. (Using only blocks of
one of those types could do that too. Kconfig uses both building blocks.
And in practice we always see blocks of both types involved when we make
Kconfig run in circles.)

What would a SAT solver do once it makes the obvious observation that
certain combinations of these two building blocks are circular?

> +but until then, Kconfig is limitted to require developers to use one of
> +the above two mechanisms to address recursive dependency issues. For more
> +details you can refer to this thread and discussion:
> +
> +http://lkml.kernel.org/r/1432241149-8762-1-git-send-email-mcgrof@do-not-panic.com

> --- a/scripts/kconfig/symbol.c
> +++ b/scripts/kconfig/symbol.c
> @@ -1117,6 +1117,8 @@ static void sym_check_print_recursive(struct

> +			fprintf(stderr, "For a resolution refer to Documentation/kbuild/kconfig-language.txt\n");
> +			fprintf(stderr, "section \"Kconfig recursive dependency limitations\"\n");

Nit: subsection.

Sorry for being so verbose. And thanks for doing this!


Paul Bolle


sample of solutions for recursive dependency errors
===================================================

21 commits contain the quote "recursive dependency detected". They
contain 22 fixes for 21 errors. (One error was solved twice. One commit
contained two fixes.)

All errors appear to involve one or more select's and one or more depend
on's.

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.

Re: [PATCH] kbuild: document recursive dependency limitation / resolution

[Luis R. Rodriguez]

On Wed, Aug 05, 2015 at 01:57:20PM +0200, Paul Bolle wrote:
> > --- a/Documentation/kbuild/kconfig-language.txt
> > +++ b/Documentation/kbuild/kconfig-language.txt
> > @@ -393,3 +393,25 @@ 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
> > +dependency resolution,
> 
> (True. But what could Kconfig do other than note that a chain of
> select's and depend on's makes it run in circles? See below.)

That's the purpose of the documentation. To annotate as TODO to
hopefuly enthusiastic kconfig developers what would need to be
looked into, some small reference material, and obviously something
for the lazy driver developer who just wants to fix the problem within
what has been discussed and accepted.

> >  this has a few implications for Kconfig file writers. In
> > +practice it means that for instance if a driver A selects a few kconfig symbols
> > +another driver B which selects any of these symbols cannot negate any of the
> > +symbols the driver A selected.
> 
> I'm afraid I don't follow this.

You're right this could use a bit more lengthy description. Can you help?
How about:

If a driver A selects a series of features, and driver B selects its own set of
features, if both have a common selected feature, they then cannot negate each
other's features. This means that we have an ongoing lump sum of intersection
of features and this is always the largest collection of features.

I gave an example for you a while ago, below I provide it again to explain.
I will note you provided your own other example, I still like and prefer mine.
They're both similar, thought. We could perhaps combine? The shorter the
better.

Example extracted from: http://lkml.kernel.org/r/20150507182838.GA20018@wotan.suse.de
-------------------------------------------------------------------------------
Let's say rock climbers hate locker rooms, but swimmer need them. We can
then have:

config GYM
        tristate
        default n

config LOCKER
        tristate
        default n
        depends on GYM

config SWIMMING
        tristate
        default n
        select GYM
        select LOCKER

config ROCK_CLIMBING
        tristate
        default n
        depends on !LOCKER
        select GYM

Kbuild seems to believe that because swimmers need lockers that rock climbers
need them too. That is obviously not true.

mcgrof@ergon ~/linux-next (git::your-swimming-dad)$ make allnoconfig
scripts/kconfig/conf --allnoconfig Kconfig
drivers/crypto/qat/Kconfig:25:error: recursive dependency detected!
drivers/crypto/qat/Kconfig:25:  symbol GYM is selected by ROCK_CLIMBING
drivers/crypto/qat/Kconfig:40:  symbol ROCK_CLIMBING depends on LOCKER
drivers/crypto/qat/Kconfig:29:  symbol LOCKER depends on GYM
#
# configuration written to .config
-------------------------------------------------------------------------------

> > +who run into this type of recursive dependency issue have two diverging
> > +options:
> > +
> > +  a) Either swap all "select FOO" to "depends on FOO" or,
> 
> all? "one or more" perhaps.

No I mean all, so in the above example the solution would be to switch
all select GYM to depends on GYM. One concrete example here was the
firmware issue with crypto stuff I was trying to add, ie firmware signing,
and a conflict with a driver I had. One option was to change all "select FW_LOADER"
to "depends on FW_LOADER" but since that was redundant given FW_LOADER is prevalent
my original proposed patch was to just remove all FW_LOADER selects [0]. Since
this was a lot of churn, I decided to go with option documented b) below.

[0] http://lkml.kernel.org/r/1432241149-8762-1-git-send-email-mcgrof@do-not-panic.com

> > +  b) Change the offending "depends on FOO" to "select FOO"
> 
> "the offending"? We're looking at a circle. So maybe:
>     Change one or more "depends on BAR" to "select BAR"   

The conflict would come up with *new* code so what I mean by
offending is to change the incoming code's use of "depends on"
to "select BAR".

> Which are both variations on a theme: stop running in circles. See below
> for a (too?) small sample of 22 solutions I could easily find in git's
> log. Swapping one or more select's with depend on's was done in two
> thirds of these solutions.

It may help to document this is the preferrred solution. This was the same
option I went with as well.

> > +Kconfig's limitations can be addressed by implementing a SAT solver for it,
> 
> Unlike Josh, I'm not familiar with SAT solvers, so it's hard to comment
> on this.
> 
> But given the two building blocks involved:
>     depends on
>     select
> 
> it's clear you can make Kconfig run in circles. (Using only blocks of
> one of those types could do that too. Kconfig uses both building blocks.
> And in practice we always see blocks of both types involved when we make
> Kconfig run in circles.)
> 
> What would a SAT solver do once it makes the obvious observation that
> certain combinations of these two building blocks are circular?

I think that's outside of the scope of the required documentation but
leave it to Josh or James to chime in if they wish.

> > +but until then, Kconfig is limitted to require developers to use one of
> > +the above two mechanisms to address recursive dependency issues. For more
> > +details you can refer to this thread and discussion:
> > +
> > +http://lkml.kernel.org/r/1432241149-8762-1-git-send-email-mcgrof@do-not-panic.com
> 
> > --- a/scripts/kconfig/symbol.c
> > +++ b/scripts/kconfig/symbol.c
> > @@ -1117,6 +1117,8 @@ static void sym_check_print_recursive(struct
> 
> > +			fprintf(stderr, "For a resolution refer to Documentation/kbuild/kconfig-language.txt\n");
> > +			fprintf(stderr, "section \"Kconfig recursive dependency limitations\"\n");
> 
> Nit: subsection.

Will change thanks.

> Sorry for being so verbose. And thanks for doing this!
> 
> 
> Paul Bolle
> 
> 
> sample of solutions for recursive dependency errors
> ===================================================
> 
> 21 commits contain the quote "recursive dependency detected". They
> contain 22 fixes for 21 errors. (One error was solved twice. One commit
> contained two fixes.)
> 
> All errors appear to involve one or more select's and one or more depend
> on's.
> 
> 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.

Maybe I'll tack this on.

  Luis

Re: [PATCH] kbuild: document recursive dependency limitation / resolution

[Paul Bolle]

Hi Luis,

(This landed in my Inbox when I was away from keyboard for a few weeks.
And then I dragged my feet a bit in answering this. Sorry about that.)

On ma, 2015-08-10 at 20:57 +0200, Luis R. Rodriguez wrote:
> On Wed, Aug 05, 2015 at 01:57:20PM +0200, Paul Bolle wrote:
> You're right this could use a bit more lengthy description. Can you help?

I'll try.

> How about:
> 
> If a driver A selects a series of features, and driver B selects its own set of
> features, if both have a common selected feature, they then cannot negate each
> other's features. This means that we have an ongoing lump sum of intersection
> of features and this is always the largest collection of features.
> 
> I gave an example for you a while ago, below I provide it again to explain.
> I will note you provided your own other example, I still like and prefer mine.
> They're both similar, thought. We could perhaps combine? The shorter the
> better.

I'll paste a condensed version of your example at the end of this
message. It triggers the same error. But perhaps it's too obvious to
serve as an example.

> Example extracted from: http://lkml.kernel.org/r/20150507182838.GA20018@wotan.suse.de
> -------------------------------------------------------------------------------
> Let's say rock climbers hate locker rooms, but swimmer need them. We can
> then have:
> 
> config GYM
>         tristate
>         default n
> 
> config LOCKER
>         tristate
>         default n
>         depends on GYM
> 
> config SWIMMING
>         tristate
>         default n
>         select GYM
>         select LOCKER
> 
> config ROCK_CLIMBING
>         tristate
>         default n
>         depends on !LOCKER
>         select GYM
> 
> Kbuild seems to believe that because swimmers need lockers that rock climbers
> need them too. That is obviously not true.

(Could it be that the translation of
	config ROCK_CLIMBING
		depends on !LOCKER

into
	symbol ROCK_CLIMBING depends on LOCKER

is a bit confusing here?)

> mcgrof@ergon ~/linux-next (git::your-swimming-dad)$ make allnoconfig
> scripts/kconfig/conf --allnoconfig Kconfig
> drivers/crypto/qat/Kconfig:25:error: recursive dependency detected!
> drivers/crypto/qat/Kconfig:25:  symbol GYM is selected by ROCK_CLIMBING
> drivers/crypto/qat/Kconfig:40:  symbol ROCK_CLIMBING depends on LOCKER
> drivers/crypto/qat/Kconfig:29:  symbol LOCKER depends on GYM

I'll go through this example step by step (I haven't peeked at my
previous attempt and hope this new explanation is a bit clearer).

"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.

For example, what values are possible for GYM? ROCK_CLIMBING selects
GYM, which means that it influences the values that are possible for
GYM. (Eg, if ROCK_CLIMBING is 'y', GYM must be 'y' too.)

What influences ROCK_CLIMBING? ROCK_CLIMBING depends on !LOCKER. (So if
LOCKER is 'y' ROCK_CLIMBING can not be set.)

And what influences LOCKER? Well, LOCKER depends on GYM, so GYM
influences LOCKER.

But that is a problem. Because this means that in order to determine
what values are possible for GYM we need to look at GYM itself. In other
words, answering that question would make the kconfig tools run in a
circle. So the kconfig tools return the "recursive dependency detected"
error instead."

(Note that SWIMMING doesn't matter for this analysis.)

> #
> # configuration written to .config
> -------------------------------------------------------------------------------

> > Which are both variations on a theme: stop running in circles. See below
> > for a (too?) small sample of 22 solutions I could easily find in git's
> > log. Swapping one or more select's with depend on's was done in two
> > thirds of these solutions.
> 
> It may help to document this is the preferrred solution. This was the same
> option I went with as well.

Yes, I like your idea to offer one or more simple guidelines. I think we
just disagree on their wording. Perhaps it's just that I've looked into
all this kconfig stuff too often already to still be able to see how
other people might think about that dreaded recursive dependency error.

Thanks,


Paul Bolle

$ cat Kconfig.locker 
# test with 'make KBUILD_KCONFIG=Kconfig.locker menuconfig'
mainmenu "Luis' locker"

config GYM
	tristate

config LOCKER
	tristate
	depends on GYM

config ROCK_CLIMBING
	tristate
	depends on LOCKER
        select GYM

Re: [PATCH] kbuild: document recursive dependency limitation / resolution

[Luis R. Rodriguez]

On Thu, Sep 3, 2015 at 4:56 AM, Paul Bolle <pebolle@tiscali.nl> wrote:
> Hi Luis,
>
> (This landed in my Inbox when I was away from keyboard for a few weeks.
> And then I dragged my feet a bit in answering this. Sorry about that.)

No worries.

> On ma, 2015-08-10 at 20:57 +0200, Luis R. Rodriguez wrote:
>> On Wed, Aug 05, 2015 at 01:57:20PM +0200, Paul Bolle wrote:
>> You're right this could use a bit more lengthy description. Can you help?
>
> I'll try.
>
>> How about:
>>
>> If a driver A selects a series of features, and driver B selects its own set of
>> features, if both have a common selected feature, they then cannot negate each
>> other's features. This means that we have an ongoing lump sum of intersection
>> of features and this is always the largest collection of features.
>>
>> I gave an example for you a while ago, below I provide it again to explain.
>> I will note you provided your own other example, I still like and prefer mine.
>> They're both similar, thought. We could perhaps combine? The shorter the
>> better.
>
> I'll paste a condensed version of your example at the end of this
> message. It triggers the same error. But perhaps it's too obvious to
> serve as an example.
>
>> Example extracted from: http://lkml.kernel.org/r/20150507182838.GA20018@wotan.suse.de
>> -------------------------------------------------------------------------------
>> Let's say rock climbers hate locker rooms, but swimmer need them. We can
>> then have:
>>
>> config GYM
>>         tristate
>>         default n
>>
>> config LOCKER
>>         tristate
>>         default n
>>         depends on GYM
>>
>> config SWIMMING
>>         tristate
>>         default n
>>         select GYM
>>         select LOCKER
>>
>> config ROCK_CLIMBING
>>         tristate
>>         default n
>>         depends on !LOCKER
>>         select GYM
>>
>> Kbuild seems to believe that because swimmers need lockers that rock climbers
>> need them too. That is obviously not true.
>
> (Could it be that the translation of
>         config ROCK_CLIMBING
>                 depends on !LOCKER
>
> into
>         symbol ROCK_CLIMBING depends on LOCKER
>
> is a bit confusing here?)

For your example alternative? Well its just a different concise
example, that's all. I understand now our differences which I'll
explain below.

>> mcgrof@ergon ~/linux-next (git::your-swimming-dad)$ make allnoconfig
>> scripts/kconfig/conf --allnoconfig Kconfig
>> drivers/crypto/qat/Kconfig:25:error: recursive dependency detected!
>> drivers/crypto/qat/Kconfig:25:  symbol GYM is selected by ROCK_CLIMBING
>> drivers/crypto/qat/Kconfig:40:  symbol ROCK_CLIMBING depends on LOCKER
>> drivers/crypto/qat/Kconfig:29:  symbol LOCKER depends on GYM
>
> I'll go through this example step by step (I haven't peeked at my
> previous attempt and hope this new explanation is a bit clearer).
>
> "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.
>
> For example, what values are possible for GYM? ROCK_CLIMBING selects
> GYM, which means that it influences the values that are possible for
> GYM. (Eg, if ROCK_CLIMBING is 'y', GYM must be 'y' too.)
>
> What influences ROCK_CLIMBING? ROCK_CLIMBING depends on !LOCKER. (So if
> LOCKER is 'y' ROCK_CLIMBING can not be set.)
>
> And what influences LOCKER? Well, LOCKER depends on GYM, so GYM
> influences LOCKER.
>
> But that is a problem. Because this means that in order to determine
> what values are possible for GYM we need to look at GYM itself. In other
> words, answering that question would make the kconfig tools run in a
> circle. So the kconfig tools return the "recursive dependency detected"
> error instead."
>
> (Note that SWIMMING doesn't matter for this analysis.)

Ah but there lies our difference, you see you are trying to just
explain *why* and *what* a recursive issue is, I'm trying to explain a
very common type of issue that can creep up. I think we should
document both. Your example just tries to go word by word by word
tying to explain *why* and how we end up in a loop, I'm trying to show
a practical issue that is implicated by the recursive issue. My
example clearly shows a limitation as well that folks have to be aware
of.

>> #
>> # configuration written to .config
>> -------------------------------------------------------------------------------
>
>> > Which are both variations on a theme: stop running in circles. See below
>> > for a (too?) small sample of 22 solutions I could easily find in git's
>> > log. Swapping one or more select's with depend on's was done in two
>> > thirds of these solutions.
>>
>> It may help to document this is the preferrred solution. This was the same
>> option I went with as well.
>
> Yes, I like your idea to offer one or more simple guidelines. I think we
> just disagree on their wording. Perhaps it's just that I've looked into
> all this kconfig stuff too often already to still be able to see how
> other people might think about that dreaded recursive dependency error.

I'll respin, include both examples to first include your example and
walk people over the recursive issue, and then provide my example to
show the implications for features on drivers. I'll also now include
some references to SAT solver solution stuff for the eager beaver that
may want to try to solve these issues.

 Luis

Re: [PATCH] kbuild: document recursive dependency limitation / resolution

[Luis R. Rodriguez]

On Thu, Sep 03, 2015 at 01:56:49PM +0200, Paul Bolle wrote:
> Hi Luis,
> 
> (This landed in my Inbox when I was away from keyboard for a few weeks.
> And then I dragged my feet a bit in answering this. Sorry about that.)

No worries I will note that I try to be as thorough so sadly this can go on
forever... I've taken your feedback and placed it first to explain *why* this
happens, then I added another subsection explaining one practical ramification
of such issue. Lastly I've exanded the patch with some homework for folks to
consider.

  Luis

[PATCH v3] kbuild: document recursive dependency limitation / resolution

[Luis R. Rodriguez]

From: "Luis R. Rodriguez" <mcgrof@suse.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@linux-m68k.org>
Cc: James Bottomley <jbottomley@odin.com>
Cc: Josh Triplett <josh@joshtriplett.org>
Cc: Paul Bolle <pebolle@tiscali.nl>
Cc: Herbert Xu <herbert@gondor.apana.org.au>
Cc: Takashi Iwai <tiwai@suse.de>
Cc: "Yann E. MORIN" <yann.morin.1998@free.fr>
Cc: Michal Marek <mmarek@suse.com>
Cc: Jonathan Corbet <corbet@lwn.net>
Cc: Mate Soos <soos.mate@gmail.com>
Cc: linux-kbuild@vger.kernel.org
Cc: linux-doc@vger.kernel.org
Cc: linux-kernel@vger.kernel.org
Signed-off-by: Luis R. Rodriguez <mcgrof@suse.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
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
+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
+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.
+
+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.
+
+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
+
+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/
diff --git a/scripts/kconfig/symbol.c b/scripts/kconfig/symbol.c
index 50878dc025a5..25cf0c2c0c79 100644
--- a/scripts/kconfig/symbol.c
+++ b/scripts/kconfig/symbol.c
@@ -1116,6 +1116,8 @@ static void sym_check_print_recursive(struct symbol *last_sym)
 		if (stack->sym == last_sym)
 			fprintf(stderr, "%s:%d:error: recursive dependency detected!\n",
 				prop->file->name, prop->lineno);
+			fprintf(stderr, "For a resolution refer to Documentation/kbuild/kconfig-language.txt\n");
+			fprintf(stderr, "subsection \"Kconfig recursive dependency limitations\"\n");
 		if (stack->expr) {
 			fprintf(stderr, "%s:%d:\tsymbol %s %s value contains %s\n",
 				prop->file->name, prop->lineno,
-- 
2.4.3

Re: [PATCH v3] kbuild: document recursive dependency limitation / resolution

[Valentin Rothberg]

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.  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.  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).

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.

On Sep 23 '15 09:41, Luis R. Rodriguez wrote:
> From: "Luis R. Rodriguez" <mcgrof@suse.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@linux-m68k.org>
> Cc: James Bottomley <jbottomley@odin.com>
> Cc: Josh Triplett <josh@joshtriplett.org>
> Cc: Paul Bolle <pebolle@tiscali.nl>
> Cc: Herbert Xu <herbert@gondor.apana.org.au>
> Cc: Takashi Iwai <tiwai@suse.de>
> Cc: "Yann E. MORIN" <yann.morin.1998@free.fr>
> Cc: Michal Marek <mmarek@suse.com>
> Cc: Jonathan Corbet <corbet@lwn.net>
> Cc: Mate Soos <soos.mate@gmail.com>
> Cc: linux-kbuild@vger.kernel.org
> Cc: linux-doc@vger.kernel.org
> Cc: linux-kernel@vger.kernel.org
> Signed-off-by: Luis R. Rodriguez <mcgrof@suse.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.

> 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.

> +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

> +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.  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.

> +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.

> +
> +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

> +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/

Thanks again for all your work,
  Valentin

Re: [PATCH v3] kbuild: document recursive dependency limitation / resolution

[Luis R. Rodriguez]

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?

> 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.

> 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.

> 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.

> On Sep 23 '15 09:41, Luis R. Rodriguez wrote:
> > From: "Luis R. Rodriguez" <mcgrof@suse.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@linux-m68k.org>
> > Cc: James Bottomley <jbottomley@odin.com>
> > Cc: Josh Triplett <josh@joshtriplett.org>
> > Cc: Paul Bolle <pebolle@tiscali.nl>
> > Cc: Herbert Xu <herbert@gondor.apana.org.au>
> > Cc: Takashi Iwai <tiwai@suse.de>
> > Cc: "Yann E. MORIN" <yann.morin.1998@free.fr>
> > Cc: Michal Marek <mmarek@suse.com>
> > Cc: Jonathan Corbet <corbet@lwn.net>
> > Cc: Mate Soos <soos.mate@gmail.com>
> > Cc: linux-kbuild@vger.kernel.org
> > Cc: linux-doc@vger.kernel.org
> > Cc: linux-kernel@vger.kernel.org
> > Signed-off-by: Luis R. Rodriguez <mcgrof@suse.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?

> > 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?

> > +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?

>  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.

> > +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.

> > +
> > +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

Re: [PATCH v3] kbuild: document recursive dependency limitation / resolution

[Valentin Rothberg]

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@suse.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@linux-m68k.org>
> > > Cc: James Bottomley <jbottomley@odin.com>
> > > Cc: Josh Triplett <josh@joshtriplett.org>
> > > Cc: Paul Bolle <pebolle@tiscali.nl>
> > > Cc: Herbert Xu <herbert@gondor.apana.org.au>
> > > Cc: Takashi Iwai <tiwai@suse.de>
> > > Cc: "Yann E. MORIN" <yann.morin.1998@free.fr>
> > > Cc: Michal Marek <mmarek@suse.com>
> > > Cc: Jonathan Corbet <corbet@lwn.net>
> > > Cc: Mate Soos <soos.mate@gmail.com>
> > > Cc: linux-kbuild@vger.kernel.org
> > > Cc: linux-doc@vger.kernel.org
> > > Cc: linux-kernel@vger.kernel.org
> > > Signed-off-by: Luis R. Rodriguez <mcgrof@suse.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

Re: [PATCH v3] kbuild: document recursive dependency limitation / resolution

[Paul Bolle]

Hi Valentin,

On di, 2015-10-06 at 10:19 +0200, Valentin Rothberg wrote:
> I think that a general remark that using selects should be discouraged
> as, besides causing the recursive issue, selects can also break
> dependencies.

How do selects break dependencies?


Paul Bolle

Re: [PATCH v3] kbuild: document recursive dependency limitation / resolution

[Valentin Rothberg]

[-- Attachment #1: Type: text/plain, Size: 1020 bytes --]

Hi Paul,

On Oct 06 '15 10:32, Paul Bolle wrote:
> Hi Valentin,
> 
> On di, 2015-10-06 at 10:19 +0200, Valentin Rothberg wrote:
> > I think that a general remark that using selects should be discouraged
> > as, besides causing the recursive issue, selects can also break
> > dependencies.
> 
> How do selects break dependencies?

Consider the following example (I also attached it as a path):

config A
    bool "CONFIG A"

config B
    bool "CONFIG B"
    depends on !A

config C
    bool "CONFIG C"
    depends on A
    select B

The option B and C are clearly contradicting with respect to A.
However, when A is set, C can be set as well because Kconfig does not
visit the dependencies of the select target (in this case B).  And since
Kconfig does not visit the dependencies, it breaks the dependencies of B
(!A).

You can test the example after applying the patch via:
   $ make KBUILD_KCONFIG=bad_selects.Kconfig menuconfig

Set A, then set C and you'll see that B is set to 'y' as well.

Kind regards,
  Valentin

[-- Attachment #2: bad_selects.patch --]
[-- Type: text/x-diff, Size: 314 bytes --]

diff --git a/bad_selects.Kconfig b/bad_selects.Kconfig
new file mode 100644
index 000000000000..989fc4e1fc17
--- /dev/null
+++ b/bad_selects.Kconfig
@@ -0,0 +1,11 @@
+config A
+    bool "CONFIG A"
+
+config B
+    bool "CONFIG B"
+    depends on !A
+
+config C
+    bool "CONFIG C"
+    depends on A
+    select B

Re: [PATCH v3] kbuild: document recursive dependency limitation / resolution

[Luis R. Rodriguez]

On Tue, Oct 6, 2015 at 2:22 AM, Valentin Rothberg
<valentinrothberg@gmail.com> wrote:
> Hi Paul,
>
> On Oct 06 '15 10:32, Paul Bolle wrote:
>> Hi Valentin,
>>
>> On di, 2015-10-06 at 10:19 +0200, Valentin Rothberg wrote:
>> > I think that a general remark that using selects should be discouraged
>> > as, besides causing the recursive issue, selects can also break
>> > dependencies.
>>
>> How do selects break dependencies?
>
> Consider the following example (I also attached it as a path):
>
> config A
>     bool "CONFIG A"
>
> config B
>     bool "CONFIG B"
>     depends on !A
>
> config C
>     bool "CONFIG C"
>     depends on A
>     select B
>
> The option B and C are clearly contradicting with respect to A.
> However, when A is set, C can be set as well because Kconfig does not
> visit the dependencies of the select target (in this case B).  And since
> Kconfig does not visit the dependencies, it breaks the dependencies of B
> (!A).
>
> You can test the example after applying the patch via:
>    $ make KBUILD_KCONFIG=bad_selects.Kconfig menuconfig
>
> Set A, then set C and you'll see that B is set to 'y' as well.

I'll add a form of this example into my patch as well... I'll respin
next. I've decided to take out all of the SAT solving discussion and
text and throw it into a wiki. We now also have quite a bit of
interest from mentors and at least one developer who might be
interested in this work. I'll Cc them and provide the wiki URL and
mailing list that can be used for further discussions / ideas on SAT
solver - kconfig integration.

 Luis

 Luis

Re: [PATCH v3] kbuild: document recursive dependency limitation / resolution

[Paul Bolle]

On di, 2015-10-06 at 01:03 +0200, Luis R. Rodriguez wrote:
> On Sun, Oct 04, 2015 at 03:42:47PM +0200, Valentin Rothberg wrote:

> > 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.

(This might be going off on a tangent a bit.)

Perhaps the issue that people run into, and that Luis is trying to
solve, here and in other threads, is that these two approaches currently
are used at the same level. In other words, maybe the configuration
requirements should only be described using dependency relations while a
(new) tool should provide what now is provided, sort of, by selects.

Isn't that how package managers work? The packages themselves state
things like: "I need Foo", "I conflict with Bar". Package managers use
that information to handle what people actually care about, like "Please
install Baz", without requiring those people to do the busy work of
figuring out the dependencies of all packages.

So, would a future SAT solver for Kconfig use a two level approach too:
given the set of dependencies of the various features (first level) try
to figure out if and how the features a user picks can actually be
enabled (second level)?

Thanks,


Paul Bolle

[PATCH v4] kbuild: document recursive dependency limitation / resolution

[Luis R. Rodriguez]

From: "Luis R. Rodriguez" <mcgrof@suse.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. If you're interested in this work or prospects
of it check out the kconfig-sat project wiki [0] and mailing list [1].

[0] http://kernelnewbies.org/KernelProjects/kconfig-sat
[1] https://groups.google.com/d/forum/kconfig-sat

Cc: Geert Uytterhoeven <geert@linux-m68k.org>
Cc: James Bottomley <jbottomley@odin.com>
Cc: Josh Triplett <josh@joshtriplett.org>
Cc: Paul Bolle <pebolle@tiscali.nl>
Cc: Herbert Xu <herbert@gondor.apana.org.au>
Cc: Takashi Iwai <tiwai@suse.de>
Cc: "Yann E. MORIN" <yann.morin.1998@free.fr>
Cc: Michal Marek <mmarek@suse.com>
Cc: Jonathan Corbet <corbet@lwn.net>
Cc: Mate Soos <soos.mate@gmail.com>
Cc: linux-kbuild@vger.kernel.org
Cc: linux-doc@vger.kernel.org
Cc: linux-kernel@vger.kernel.org
Signed-off-by: Luis R. Rodriguez <mcgrof@suse.com>
---
 Documentation/kbuild/Kconfig.recursion-issue-01 |  57 +++++++++
 Documentation/kbuild/Kconfig.recursion-issue-02 |  63 ++++++++++
 Documentation/kbuild/Kconfig.select-break       |  33 +++++
 Documentation/kbuild/kconfig-language.txt       | 161 ++++++++++++++++++++++++
 scripts/kconfig/symbol.c                        |   2 +
 5 files changed, 316 insertions(+)
 create mode 100644 Documentation/kbuild/Kconfig.recursion-issue-01
 create mode 100644 Documentation/kbuild/Kconfig.recursion-issue-02
 create mode 100644 Documentation/kbuild/Kconfig.select-break

diff --git a/Documentation/kbuild/Kconfig.recursion-issue-01 b/Documentation/kbuild/Kconfig.recursion-issue-01
new file mode 100644
index 000000000000..e8877db0461f
--- /dev/null
+++ b/Documentation/kbuild/Kconfig.recursion-issue-01
@@ -0,0 +1,57 @@
+# Simple Kconfig recursive issue
+# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+#
+# 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.
+
+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..b9fd56c4b57e
--- /dev/null
+++ b/Documentation/kbuild/Kconfig.recursion-issue-02
@@ -0,0 +1,63 @@
+# Cumulative Kconfig recursive issue
+# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+#
+# 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 here. 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". Another
+# more important reason is that kconfig does not check for dependencies listed
+# under 'select' for a symbol, when such symbols are selected kconfig them
+# as mandatory required symbols. For more details on the heavy handed nature
+# of select refer to Documentation/kbuild/Kconfig.select-break
+#
+# 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
+
+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
diff --git a/Documentation/kbuild/Kconfig.select-break b/Documentation/kbuild/Kconfig.select-break
new file mode 100644
index 000000000000..365ceb3424b1
--- /dev/null
+++ b/Documentation/kbuild/Kconfig.select-break
@@ -0,0 +1,33 @@
+# Select broken dependency issue
+# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+#
+# Test with:
+#
+# make KBUILD_KCONFIG=Documentation/kbuild/Kconfig.select-break menuconfig
+#
+# kconfig will not complain and enable this layout for configuration. This is
+# currently a feature of kconfig, given select was designed to be heavy handed.
+# Kconfig currently does not check the list of symbols listed on a symbol's
+# "select" list, this is done on purpose to help load a set of known required
+# symbols. Because of this use of select should be used with caution. An
+# example of this issue is below.
+#
+# The option B and C are clearly contradicting with respect to A.
+# However, when A is set, C can be set as well because Kconfig does not
+# visit the dependencies of the select target (in this case B).  And since
+# Kconfig does not visit the dependencies, it breaks the dependencies of B
+# (!A).
+
+mainmenu "Simple example to demo kconfig select broken dependency issue"
+
+config A
+	bool "CONFIG A"
+
+config B
+	bool "CONFIG B"
+	depends on !A
+
+config C
+	bool "CONFIG C"
+	depends on A
+	select B
diff --git a/Documentation/kbuild/kconfig-language.txt b/Documentation/kbuild/kconfig-language.txt
index 350f733bf2c7..c52856da0cad 100644
--- a/Documentation/kbuild/kconfig-language.txt
+++ b/Documentation/kbuild/kconfig-language.txt
@@ -393,3 +393,164 @@ 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, a recursive dependency can be
+summarized as a circular dependency. The kconfig tools need to ensure that
+Kconfig files comply with specified configuration requirements. In order to do
+that kconfig must determine the values that are possible for all Kconfig
+symbols, this is currently not possible if there is a circular relation
+between two or more Kconfig symbols. For more details refer to the "Simple
+Kconfig recursive issue" subsection below. Kconfig does not do recursive
+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
+subsections.
+
+Simple Kconfig recursive issue
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Read: Documentation/kbuild/Kconfig.recursion-issue-01
+
+Test with:
+
+make KBUILD_KCONFIG=Documentation/kbuild/Kconfig.recursion-issue-01 allnoconfig
+
+Cumulative Kconfig recursive issue
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Read: Documentation/kbuild/Kconfig.recursion-issue-02
+
+Test with:
+
+make KBUILD_KCONFIG=Documentation/kbuild/Kconfig.recursion-issue-02 allnoconfig
+
+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.
+
+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
+
+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]. Another known related project
+is CADOS [2] (former VAMOS [3]) and the tools, mainly undertaker [4], which has
+been introduced first with [5].  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. If using a SAT solver is
+desirable on Kconfig one approach would be to evaluate repurposing such efforts
+somehow on Kconfig. There is enough interest from mentors of existing projects
+to not only help advise how to integrate this work upstream but also help
+maintain it long term. Interested developers should visit:
+
+http://kernelnewbies.org/KernelProjects/kconfig-sat
+
+[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] https://cados.cs.fau.de
+[3] https://vamos.cs.fau.de
+[4] https://undertaker.cs.fau.de
+[5] https://www4.cs.fau.de/Publications/2011/tartler_11_eurosys.pdf
diff --git a/scripts/kconfig/symbol.c b/scripts/kconfig/symbol.c
index 50878dc025a5..25cf0c2c0c79 100644
--- a/scripts/kconfig/symbol.c
+++ b/scripts/kconfig/symbol.c
@@ -1116,6 +1116,8 @@ static void sym_check_print_recursive(struct symbol *last_sym)
 		if (stack->sym == last_sym)
 			fprintf(stderr, "%s:%d:error: recursive dependency detected!\n",
 				prop->file->name, prop->lineno);
+			fprintf(stderr, "For a resolution refer to Documentation/kbuild/kconfig-language.txt\n");
+			fprintf(stderr, "subsection \"Kconfig recursive dependency limitations\"\n");
 		if (stack->expr) {
 			fprintf(stderr, "%s:%d:\tsymbol %s %s value contains %s\n",
 				prop->file->name, prop->lineno,
-- 
2.4.3

Re: [PATCH v4] kbuild: document recursive dependency limitation / resolution

[Michal Marek]

On Wed, Oct 07, 2015 at 04:16:33PM -0700, Luis R. Rodriguez wrote:
> From: "Luis R. Rodriguez" <mcgrof@suse.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. If you're interested in this work or prospects
> of it check out the kconfig-sat project wiki [0] and mailing list [1].
> 
> [0] http://kernelnewbies.org/KernelProjects/kconfig-sat
> [1] https://groups.google.com/d/forum/kconfig-sat
> 
> Cc: Geert Uytterhoeven <geert@linux-m68k.org>
> Cc: James Bottomley <jbottomley@odin.com>
> Cc: Josh Triplett <josh@joshtriplett.org>
> Cc: Paul Bolle <pebolle@tiscali.nl>
> Cc: Herbert Xu <herbert@gondor.apana.org.au>
> Cc: Takashi Iwai <tiwai@suse.de>
> Cc: "Yann E. MORIN" <yann.morin.1998@free.fr>
> Cc: Michal Marek <mmarek@suse.com>
> Cc: Jonathan Corbet <corbet@lwn.net>
> Cc: Mate Soos <soos.mate@gmail.com>
> Cc: linux-kbuild@vger.kernel.org
> Cc: linux-doc@vger.kernel.org
> Cc: linux-kernel@vger.kernel.org
> Signed-off-by: Luis R. Rodriguez <mcgrof@suse.com>

Applied to kbuild.git#kconfig, thanks.

Michal