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@xxxxxxxx> > > > > > > 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@xxxxxxxxxxxxxx> > > > Cc: James Bottomley <jbottomley@xxxxxxxx> > > > Cc: Josh Triplett <josh@xxxxxxxxxxxxxxxx> > > > Cc: Paul Bolle <pebolle@xxxxxxxxxx> > > > Cc: Herbert Xu <herbert@xxxxxxxxxxxxxxxxxxx> > > > Cc: Takashi Iwai <tiwai@xxxxxxx> > > > Cc: "Yann E. MORIN" <yann.morin.1998@xxxxxxx> > > > Cc: Michal Marek <mmarek@xxxxxxxx> > > > Cc: Jonathan Corbet <corbet@xxxxxxx> > > > Cc: Mate Soos <soos.mate@xxxxxxxxx> > > > Cc: linux-kbuild@xxxxxxxxxxxxxxx > > > Cc: linux-doc@xxxxxxxxxxxxxxx > > > Cc: linux-kernel@xxxxxxxxxxxxxxx > > > Signed-off-by: Luis R. Rodriguez <mcgrof@xxxxxxxx> > > > --- > > > > > > 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@xxxxxxxxxxxxxxxx > > > [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@xxxxxxxxxxxxxxxx > > > + > > > +Practical solutions to kconfig recursive issue > > > +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ > > > + > > > +Developers who run into the recursive Kconfig issue have three options > > > +at their disposal. We document them below and also provide a list of > > > +historical issues resolved through these different solutions. > > > + > > > + a) Remove any superfluous "select FOO" or "depends on FOO" > > > + b) Match dependency semantics: > > > + b1) Swap all "select FOO" to "depends on FOO" or, > > > + b2) Swap all "depends on FOO" to "select FOO" > > > + > > > +The resolution to a) can be tested with the sample Kconfig file > > > +Documentation/kbuild/Kconfig.recursion-issue-01 through the removal > > > +of the "select CORE" from CORE_BELL_A_ADVANCED as that is implicit already > > > +since CORE_BELL_A depends on CORE. At times it may not be possible to remove > > > +some dependency criteria, for such cases you can work with solution b). > > > + > > > +The two different resolutions for b) can be tested in the sample Kconfig file > > > +Documentation/kbuild/Kconfig.recursion-issue-02. > > > + > > > +Below is a list of examples of prior fixes for these types of recursive issues; > > > +all errors appear to involve one or more select's and one or more "depends on". > > > + > > > +commit fix > > > +====== === > > > +06b718c01208 select A -> depends on A > > > +c22eacfe82f9 depends on A -> depends on B > > > +6a91e854442c select A -> depends on A > > > +118c565a8f2e select A -> select B > > > +f004e5594705 select A -> depends on A > > > +c7861f37b4c6 depends on A -> (null) > > > +80c69915e5fb select A -> (null) (1) > > > +c2218e26c0d0 select A -> depends on A (1) > > > +d6ae99d04e1c select A -> depends on A > > > +95ca19cf8cbf select A -> depends on A > > > +8f057d7bca54 depends on A -> (null) > > > +8f057d7bca54 depends on A -> select A > > > +a0701f04846e select A -> depends on A > > > +0c8b92f7f259 depends on A -> (null) > > > +e4e9e0540928 select A -> depends on A (2) > > > +7453ea886e87 depends on A > (null) (1) > > > +7b1fff7e4fdf select A -> depends on A > > > +86c747d2a4f0 select A -> depends on A > > > +d9f9ab51e55e select A -> depends on A > > > +0c51a4d8abd6 depends on A -> select A (3) > > > +e98062ed6dc4 select A -> depends on A (3) > > > +91e5d284a7f1 select A -> (null) > > > + > > > +(1) Partial (or no) quote of error. > > > +(2) That seems to be the gist of that fix. > > > +(3) Same error. > > > > ^ It's awesome to have list like above. > > That was thanks to Paul. Thanks Paul :-) > > > + > > > +Future kconfig work > > > +~~~~~~~~~~~~~~~~~~~ > > > + > > > +Work on kconfig is welcomed on both areas of clarifying semantics and on > > > +evaluating the use of a full SAT solver for it. A full SAT solver can be > > > +desirable to enable more complex dependency mappings and / or queries, > > > +for instance on possible use case for a SAT solver could be that of handling > > > +the current known recursive dependency issues. It is not known if this would > > > +address such issues but such evaluation is desirable. If support for a full SAT > > > +solver proves too complex or that it cannot address recursive dependency issues > > > +Kconfig should have at least clear and well defined semantics which also > > > +addresses and documents limitations or requirements such as the ones dealing > > > +with recursive dependencies. > > > + > > > +Further work on both of these areas is welcomed on Kconfig. We elaborate > > > +on both of these in the next two subsections. > > > + > > > +Semantics of Kconfig > > > +~~~~~~~~~~~~~~~~~~~~ > > > + > > > +The use of Kconfig is broad, Linux is now only one of Kconfig's users: > > > +one study has completed a broad analysis of Kconfig use in 12 projects [0]. > > > +Despite its widespread use, and although this document does a reasonable job > > > +in documenting basic Kconfig syntax a more precise definition of Kconfig > > > +semantics is welcomed. One project deduced Kconfig semantics through > > > +the use of the xconfig configurator [1]. Work should be done to confirm if > > > +the deduced semantics matches our intended Kconfig design goals. > > > + > > > +Having well defined semantics can be useful for tools for practical > > > +evaluation of depenencies, for instance one such use known case was work to > > > +express in boolean abstraction of the inferred semantics of Kconfig to > > > +translate Kconfig logic into boolean formulas and run a SAT solver on this to > > > +find dead code / features (always inactive), 114 dead features were found in > > > +Linux using this methodology [1] (Section 8: Threats to validity). > > > + > > > +Confirming this could prove useful as Kconfig stands as one of the the leading > > > +industrial variability modeling languages [1] [2]. Its study would help > > > +evaluate practical uses of such languages, their use was only theoretical > > > +and real world requirements were not well understood. As it stands though > > > +only reverse engineering techniques have been used to deduce semantics from > > > +variability modeling languages such as Kconfig [3]. > > > + > > > +[0] http://www.eng.uwaterloo.ca/~shshe/kconfig_semantics.pdf > > > +[1] http://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf > > > +[2] http://gsd.uwaterloo.ca/sites/default/files/ase241-berger_0.pdf > > > +[3] http://gsd.uwaterloo.ca/sites/default/files/icse2011.pdf > > > > A highly related project is CADOS [1] (former VAMOS [2]) and the tools, > > mainly undertaker [3], which has been introduced first with [4]. The > > basic concept of undertaker is to exract variability models from > > Kconfig, and put them together with a propositional formula extracted > > from CPP #ifdefs and build-rules into a SAT solver in order to find dead > > code, dead files, and dead symbols. > > > > [1] https://cados.cs.fau.de > > [2] https://vamos.cs.fau.de > > [3] https://undertaker.cs.fau.de > > [4] https://www4.cs.fau.de/Publications/2011/tartler_11_eurosys.pdf > > Thanks, I'll stuff that in. > > > > +Full SAT solver for Kconfig > > > +~~~~~~~~~~~~~~~~~~~~~~~~~~~ > > > + > > > +Although SAT solvers [0] haven't yet been used by Kconfig directly, as noted in > > > +the previous subsection, work has been done however to express in boolean > > > +abstraction the inferred semantics of Kconfig to translate Kconfig logic into > > > +boolean formulas and run a SAT solver on it [1]. If using a SAT solver is > > > +desirable on Kconfig one approach would be to evaluate repurposing such effort > > > +somehow on Kconfig. The 3-year Mancoosi research project [1] challenged > > > +researchers and developers with solutions for software package resolution > > > +dependencies requiring free software licenses for proposed solutions, some of > > > +the solutions proposed used SAT solvers, one of which was CryManSolver which > > > +used CryptoMiniSat [3] [4] as backend (a SAT solver in itself). CryptoMiniSat > > > +remains of the only SAT solvers which aims to be fully open that also has a > > > +relatively clean C++ / Python interface. Evaluation of CryptoMiniSat for use > > > +with Kconfig is desirable. > > > + > > > +[0] http://www.cs.cornell.edu/~sabhar/chapters/SATSolvers-KR-Handbook.pdf > > > +[1] http://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf > > > +[2] http://mancoosi.org/ > > > +[3] http://www.msoos.org/cryptominisat4/ > > > +[4] https://github.com/msoos/cryptominisat/ > > > > As mentioned in a different mail thread, undertaker uses PicoSAT [5]. I > > am no expert in SAT solving, but PicoSAT works reliably fast, it is > > written in C and also ships PicoMUS to generate a Minimally > > Unsatisfiable Subformula. We use it the MUS to understand which Kconfig > > symbols contribute to a boolean contradiction when analyzing dead > > features or dead code, etc. It is a powerful tool and could be > > interesting especially in the context of Kconfig. > > > > Hence, I suggest to add [5] to list above to consider it in future > > evaluations. > > > > [5] http://fmv.jku.at/picosat/ > > Indeed. Will do, and fortunately Armin considers this as sensible and seems > willing to help maintain such code if we end up using it on Linux. Since I > don't have time and this seems to be a generally self contained effort I think > this might be a very nicely suited project for Outreachy. I'd be up to help > mentor this work. If anyone else is please let me know. > > Unless of course someone tells me now that they're interested in doing this work > right away :) > > Luis -- To unsubscribe from this list: send the line "unsubscribe linux-doc" in the body of a message to majordomo@xxxxxxxxxxxxxxx More majordomo info at http://vger.kernel.org/majordomo-info.html
