Index: /reasoner/conclusion.tex =================================================================== --- /reasoner/conclusion.tex (revision 274) +++ /reasoner/conclusion.tex (revision 275) @@ -1,12 +1,18 @@ \section{Conclusion}\label{sectConclusion} -\TBD{We are better than before, we are now more IVML-complete, but not reasoning-complete. Future, integrate with SMT or other solvers for left-over reasoning problems or configuration completion/instance creation (potential student work).} +Reasoning support for variability models is a required capability for product line tooling environments. Many product line approaches focus on Boolean models where reasoning and model analysis is well understood~\cite{MendoncaWasowskiCzarnecki09}. However, in practice, more and more non-Boolean variabilities desired, thus, requiring respective reasoning capabilities, i.e., higher expressiveness, in some cases at the price of lower analyzability~\cite{EichelbergerKroeherSchmid13}. Hence, the provided expressiveness of a variability modeling language increases the complexity of the reasoning activities, including pre-processing or model/constraint translation. At the moment we do not aim at reasoning completeness and consider this reasoner as a first step towards a mixed reasoning approach, where further reasoning capabilities are introduced, e.g., in terms of subsequent reasoners in a reasoning chain. + +In this report, we discussed in detail a reasoning approach for the Integrated Variability Modeling Language (IVML)~\cite{IVML-LS}, aiming at both, a full coverage of the IVML concepts as well as high performance. Particular features are support for complex user-defined types, shadowed variables, and constraint variables, which, in summary, require mechanisms to explicitly or implicitly change the constraint base while reasoning. Moreover, the approach allows for two forms of incremental reasoning, one even re-using the created constraint base. We discussed the reasoning approach (Section \ref{sectApproach}), introduced basic as well as IVML related notation and terms (Section \ref{sectNotation}), and presented the main reasoning algorithms (Section \ref{sectReasoning}). As our approach instantiates constraints before reasoning to cope with the various IVML modeling concepts, a large portion (Section \ref{sectTranslation}) of this report was devoted to the constraint translation. We introduced constraint translation patterns and discussed the underlying algorithms to realize the translation. The subsequent constraint evaluation is then done in terms of a forward-chaining loop, whereby the actual expression evaluation is done by a complex software component provided by EASy-Producer. During evaluation, the need for re-scheduling individual constraint evaluations may occur, in particular when dependent values, (compound) types or constraint variables change. We presented the related algorithms in Section \ref{sectTopLevelConstraintsRescheduling}. After all algorithmic parts were introduced, we discussed the coverage of the reasoning approach with respect to the IVML modeling concepts in Section \ref{sectCompleteness}, also indicating at least one test case per required translation path. In Section \ref{sectPerformance}, we summarized performance issues identified while creating the presented reasoner. Finally, in Section \ref{sectEvaluation}, we presented a (time-based) performance evaluation comparing the intial and the presented reasoner version for different devices and JDK versions. + +This report is a fundamental building brick in the direction of reasoning for complex non-Boolean variability models. It shows that on actual devices, reasoning for such models, here exemplified for IVML, is possible fulfilling both, a complete coverage of the required modeling concepts as well as the performance. For rather large conventional models, the proposed approach even operates on a Raspberry Pi 3 in less than 50ms. Larger and more complex models, such as the QualiMaster models deserve more computational power and can currently be analyzed in around 500 ms full reasoning, 150 ms incremental reasoning and 50 ms reasoning with re-used constraint base. + +Future work will require reasoning capabilities in the embedded and IoT field, and, thus, either requires as faster reasoning approach, a native implementation of the presented approach or a performance optimization. Even for a native version, performance optimization is required. In this report, we already identified several opportunities: \begin{itemize} + \item Immediate evaluation of default value constraints and storing only initially failing assignment constraints in the constraint base. + \item IVML type caching allowing for + \item quantification unrolling \item model optimizations (see Section \ref{sectEvaluationResultsDescriptive}, Table \ref{experimentsDescSummary}) - \item execute default value assignments upon creation and throw away - \item type cache - \item quantification unrolling \end{itemize} -Pi speedup needed! +Moreover, advanced reasoning capabilities are of high interest for our work, i.e., integrating the presented reasoner as a fast initial step in a reasoning chain with other reasoning-complete approaches, such as SMT-solvers is also a possible future direction. Index: /reasoner/evaluation.tex =================================================================== --- /reasoner/evaluation.tex (revision 274) +++ /reasoner/evaluation.tex (revision 275) @@ -25,9 +25,9 @@ Several test cases of EASy-Producer involve reasoning, namely \begin{itemize} -\item the EASy-Producer test suites for the SSE reasoner (based on the \IVML{ReasonerCore} test suite). +\item the EASy-Producer test suites for the SSE reasoner (based on the \IVML{ReasonerCore} test suite). The largest conventional model was created by a generator and consists of 1500 Boolean top-level variables and 4500 constraints. \item the EASy-Producer test suite for the VIL runtime extension involving the reasoner to detect runtime deviations and to validate runtime changes in the configuration before executing them. \item scenario test cases for the BMWi ScaleLog\footnote{These test cases are not publicly available as they contain propretary knowledge of the industrial partner in the ScaleLog project.} project. -\item the EASy-Producer scenario test cases including several (historical) model variants from FP7 QualiMaster \cite{EichelbergerQinSizonenko+16}. -\item an extended set of scenario test cases derived from the largest QualiMaster models in the EASy-Producer scenario test cases. These tests were specifically defined for this experiment as the gap in model size between the QualiMaster models and the other models was too big. The QualiMaster model consists of several imported projects, various user-defined types, a topological structure for defining Big Data processing pipelines and 16 configured pipelines. This corresponds roughly to 20.000 individual variables. In the set of test cases, we created models with the same type definitions but systematically varied the number of pipelines, i.e., created projected models with one pipeline, two pipelines etc. All these models contain only the required linked variables such as algorithms or data sources so that the respective model is structurally valid and its configuration is consistent. +\item the EASy-Producer scenario test cases including several (historical) model variants from FP7 QualiMaster \cite{EichelbergerQinSizonenko+16}. The largest QualiMaster model consists of several imported projects, various user-defined types, a topological structure for Big Data processing pipelines, quantified constraints, constraint variables and 16 configured pipelines. A configuration of the latest model roughly corresponds to 16.000 individual variables. +\item an extended set of scenario test cases derived from the largest QualiMaster models in the EASy-Producer scenario test cases. These tests were specifically defined for this experiment as the gap in model size between the QualiMaster models and the other models was too big. In the set of test cases, we created models with the same type definitions but systematically varied the number of pipelines, i.e., created projected models with one pipeline, two pipelines etc. All these models contain only the required linked variables such as algorithms or data sources so that the respective model is structurally valid and its configuration is consistent. \end{itemize} We use these test cases as experimental treatments, although they involve test dependencies such as jUnit. While some of the test cases rely on programmed models (in terms of the IVML object model), most of the test cases specify the model in terms of IVML, i.e., for a more realistic setup and require for execution the IVML parser as well as dependent Eclipse libraries. As we focus on the reasoning time, the actual creation of the reasoning model shall not affect the results. @@ -41,6 +41,6 @@ As specific measurements for this evaluation, we include \begin{itemize} - \item the default statistics of the SSE reasoner, i.e., the time consumed by constraint translation (translation time), the time used for evaluating constraints (evaluation time), the time used for reasoning (including translation and constraint evaluation time), the number of failed constraints, and the number of re-evaluated constraints. - \item statistics model about the underlying model as well as the complexity measure (cf. Section \ref{sectModelComplexity}) realized by EASy-Producer. + \item the default statistics of the SSE reasoner, i.e., the time consumed by constraint translation (translation time), the time used for evaluating constraints (evaluation time), the time used for reasoning (including translation and constraint evaluation time), the number of failed constraints, and the number of re-evaluated constraints. These measures are taken while and after reasoning. + \item statistics model about the underlying model as well as the complexity measure (cf. Section \ref{sectModelComplexity}) realized by EASy-Producer. These measures are taken before reasoning. \end{itemize} @@ -302,7 +302,7 @@ \clearpage -In the diagrams, we separate visually two main groups of test cases, namely reasoning core tests and scenario tests, the latter including the tests for the ScaleLog and QualiMaster models. Both groups are sub-divided into full reasoning, incremental reasoning (partial constraint base) and runtime-reasoning (re-used partial constraint base). For each group, we indicate a (desirable) linear regression of the measurements (dotted lines) with surrounding 95\% confidence region. Depending on the reasoner version, the treatment sets differ (cf. Section \ref{sectEvalSetupTreatments}), e.g., no re-used partial constraint based tests are available for reasoner version 1.1.0 as discussed in Sections \ref{sectEvalSetupSubjects} and \ref{sectEvalSetupTreatments}. - -Figures \ref{fig:old-1_10-jdk8} and \ref{fig:old-1_30-jdk8} illustrate the measurements for the two reasoner versions on \emph{laptop \ref{oldLaptopId}} (experiment id 1 and 2). While the scale of the obtained measurements for the \textit{full reasoning} time is roughly the same for both versions (reasoner version 1.3.0 is faster as discussed in Section \ref{sectEvaluationResultsDescriptive}), the scales for translation and evaluation time differ. In other words, for reasoner version 1.3.0, translation and evaluation time sum up to the reasoning time as expected, while this does not hold for reasoner version 1.1.0. We attribute this (as also evident in the code) to additional operations performed before, between or after translation/evaluation, e.g., by unnecessary creation of configuration instances, non-incremental and superfluous freezing of IVML variables, or by output can be deferred after reasoning time (cf. Section \ref{sectPerformance}). While version 1.1.0 may appear to be faster in translation and evaluation time, it is important to recall that the translation algorithms of version 1.1.0 are not IVML-complete. Moreover, version 1.3.0 behaves more linearly, i.e., measured times, in particular reasoning time, have less deviation from the desired, while version 1.1.0 in Figure \ref{fig:old-1_10-jdk8} tends to a quadratic behavior. \textit{Incremental reasoning} for version 1.3.0 is faster than for version 1.1.0, although again, translation and evaluation in detail are slower due to a higher degree of IVML-completeness. \textit{Re-using the constraint base} by instantiating the reasoner for a certain IVML model (here just changing a few configuration variables) does not seem to allocate (much) time in translation and evaluation. In contrast, regarding total reasoning time, this form of runtime reasoning requires 20-50ms, which we attribute to the transfer of constraints between the stored and the actual constraint base. +In the diagrams, we separate visually two main groups of test cases, namely reasoning core tests and scenario tests, the latter including the tests for the ScaleLog and QualiMaster models. Both groups are sub-divided into full reasoning, incremental reasoning (partial constraint base, indicated by "inc") and runtime-reasoning (re-used partial constraint base, indicated by "rt"). The largest conventional model appears at a model complexity of 5250 in the full reasoning core tests, the largest QualiMaster model occurs at 20.000 in full scenario reasoning as well as at 25.323 (due to the already existing configuraiton) in incremental and runtime-reasoning. For each group, we indicate a (desirable) linear regression of the measurements (dotted lines) with surrounding 95\% confidence region. Depending on the reasoner version, the treatment sets differ (cf. Section \ref{sectEvalSetupTreatments}), e.g., no re-used partial constraint based tests are available for reasoner version 1.1.0 as discussed in Sections \ref{sectEvalSetupSubjects} and \ref{sectEvalSetupTreatments}. + +Figures \ref{fig:old-1_10-jdk8} and \ref{fig:old-1_30-jdk8} illustrate the measurements for the two reasoner versions on \emph{laptop \ref{oldLaptopId}} (experiment id 1 and 2). While the scale of the obtained measurements for the \textit{full reasoning} time is roughly the same for both versions (reasoner version 1.3.0 is faster as discussed in Section \ref{sectEvaluationResultsDescriptive}), the scales for translation and evaluation time differ. In other words, for reasoner version 1.3.0, translation and evaluation time sum up to the reasoning time as expected, while this does not hold for reasoner version 1.1.0. We attribute this (as also evident in the code) to additional operations performed before, between or after translation/evaluation, e.g., by unnecessary creation of configuration instances, non-incremental and superfluous freezing of IVML variables, or by output can be deferred after reasoning time (cf. Section \ref{sectPerformance}). While version 1.1.0 may appear to be faster in translation and evaluation time, it is important to recall that the translation algorithms of version 1.1.0 are not IVML-complete. Moreover, version 1.3.0 behaves more linearly, i.e., measured times, in particular reasoning time, have less deviation from the desired, while version 1.1.0 in Figure \ref{fig:old-1_10-jdk8} tends to a quadratic behavior (cf. Section \ref{sectPerformance}). \textit{Incremental reasoning} for version 1.3.0 is faster than for version 1.1.0, although again, translation and evaluation in detail are slower due to a higher degree of IVML-completeness. \textit{Re-using the constraint base} by instantiating the reasoner for a certain IVML model (here just changing a few configuration variables) does not seem to allocate (much) time in translation and evaluation. In contrast, regarding total reasoning time, this form of runtime reasoning requires 20-50ms, which we attribute to the transfer of constraints between the stored and the actual constraint base. \begin{figure}[!htb] @@ -378,3 +378,3 @@ \clearpage -In summary, we conclude that reasoner version 1.3.0 is faster than version 1.1.0 while providing more IVML-completeness and additional features such as re-using the constraint base. Also it seems that version 1.3.0 leads to less spikes, which may also be due to the underlying setup. While the achieved runtime for full reasoning on "usual" devices such as \ref{oldLaptopId}, \ref{newLaptopId} or \ref{jenkinsId} is sufficient even for runtime adaptation scenarios~\cite{Eichelberger18}, applying EASy-Producer and the IVML reasoner in embedded settings is possible, but reasoning over large models in soft realtime settings is problematic (full reasoning up to 6s, incremental about 2s and instance-based reasoning up to 1s). In this case, additional performance optimizations of the reasoner as well as the underlying model infrastructure as sketched in this report are required. +In summary, we conclude that reasoner version 1.3.0 is faster than version 1.1.0 while providing a higher IVML-completeness as well as additional features such as re-using the constraint base. Moreover, version 1.3.0 appears to behave more linearly than version 1.1.0, which tends to have a quadratic runtime behavior for larger models (cf. Section \ref{sectPerformance} for resolved algorithmic problems). Also it seems that the execution of version 1.3.0 is less spiky, which may also be due to the underlying setup. The achieved runtime for full reasoning on "usual" devices such as \ref{oldLaptopId}, \ref{newLaptopId} or \ref{jenkinsId} is sufficient for runtime adaptation scenarios even on for the larger models~\cite{Eichelberger18}. However, applying EASy-Producer and the IVML reasoner in embedded setups is possible, but reasoning over large models in soft realtime settings is problematic, as currently full reasoning takes up to 6s, incremental reasoning up to 2s and instance-based reasoning up to 1s. We are convinced that additional performance optimizations of the reasoner as well as the underlying model infrastructure as sketched in this report can allow for sufficient speed-up at least for incremental and runtime reasoning in such settings. Index: /reasoner/introduction.tex =================================================================== --- /reasoner/introduction.tex (revision 274) +++ /reasoner/introduction.tex (revision 275) @@ -14,4 +14,5 @@ \item Support for shadowed / redefined IVML compound slots, i.e., properly applying constraints for shadowed slots to the most specific slot in a compound hierarchy. \item Support for IVML constraint variables. IVML supports variables that hold a constraint, i.e., a configuration can explicitly define, add, remove or disable constraints, i.e., actively change the constraint set during reasoning. + \item Modes for full reasoning (irrespective of a given configuration, incremental reasoning as well as reasoning over configuration changes. \item Although the current reasoning approach is not reasoning complete, it is designed to act as the first step in a chained reasoning approach. For such subsequent reasoners, the IVML reasoner provides a solid basis, detailed error messages including the failed instantiated constraints so that a chained reasoner can directly continue working with these constraints. \end{itemize}