Document Open Access Logo

A Calculus for Variational Programming

Authors Sheng Chen, Martin Erwig, Eric Walkingshaw

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2016.6.pdf
  • Filesize: 0.65 MB
  • 28 pages

Document Identifiers

Author Details

Sheng Chen
Martin Erwig
Eric Walkingshaw

Cite AsGet BibTex

Sheng Chen, Martin Erwig, and Eric Walkingshaw. A Calculus for Variational Programming. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 6:1-6:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.ECOOP.2016.6

Abstract

Variation is ubiquitous in software. Many applications can benefit from making this variation explicit, then manipulating and computing with it directly---a technique we call "variational programming". This idea has been independently discovered in several application domains, such as efficiently analyzing and verifying software product lines, combining bounded and symbolic model-checking, and computing with alternative privacy profiles. Although these domains share similar core problems, and there are also many similarities in the solutions, there is no dedicated programming language support for variational programming. This makes the various implementations tedious, prone to errors, hard to maintain and reuse, and difficult to compare. In this paper we present a calculus that forms the basis of a programming language with explicit support for representing, manipulating, and computing with variation in programs and data. We illustrate how such a language can simplify the implementation of variational programming tasks. We present the syntax and semantics of the core calculus, a sound type system, and a type inference algorithm that produces principal types.
Keywords
  • Variational programming
  • variational types
  • variability-aware analyses

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. S. Apel, D. Beyer, K. Friedberger, F. Raimondi, and A. von Rhein. Domain types: Abstract-domain selection based on variable usage. In HVC, LNCS 8244, pages 262-278, 2013. Google Scholar
  2. S. Apel, C. Kästner, A. Größlinger, and C. Lengauer. Type safety for feature-oriented product lines. JASE, 17(3):251-300, 2010. Google Scholar
  3. T. H. Austin and C. Flanagan. Multiple facets for dynamic information flow. In POPL, pages 165-178, 2012. Google Scholar
  4. Andrej B. and Matija P. Programming with algebraic effects and handlers. CoRR, abs/1203.1539, 2012. Google Scholar
  5. D. Batory, J. Sarvela, and A. Rauschmayer. Scaling step-wise refinement. TSE, 30(6):355-371, 2004. Google Scholar
  6. E. Bodden, T. Tolêdo, M. Ribeiro, C. Brabrand, P. Borba, and M. Mezini. SPL^LIFT: Statically analyzing software product lines in minutes instead of years. In PLDI, pages 355-364, 2013. Google Scholar
  7. C. Brabrand, M. Ribeiro, T. Tolêdo, and Paulo B. Intraprocedural dataflow analysis for software product lines. In AOSD, pages 13-24, 2012. Google Scholar
  8. E. Brady. Programming and reasoning with algebraic effects and dependent types. In ICFP, pages 133-144, 2013. Google Scholar
  9. R. Capizzi, A. Longo, V. N. Venkatakrishnan, and A. P. Sistla. Preventing information leaks through shadow executions. In ACSAC, pages 322-331, 2008. Google Scholar
  10. S. Chen and M. Erwig. Counter-factual typing for debugging type errors. In POPL, pages 583-594, 2014. Google Scholar
  11. S. Chen and M. Erwig. Early detection of type errors in C++ templates. In PEPM, pages 133-144, 2014. Google Scholar
  12. S. Chen and M. Erwig. Guided type debugging. In FLOPS, LNCS 8475, pages 35-51. 2014. Google Scholar
  13. S. Chen and M. Erwig. Type-based parametric analysis of program families. In ICFP, pages 39-51, 2014. Google Scholar
  14. S. Chen and M. Erwig. Principal type inference for GADTs. In POPL, pages 416-428, 2016. Google Scholar
  15. S. Chen, M. Erwig, and K. Smeltzer. Let’s hear both sides: On combining type-error reporting tools. In VL/HCC, pages 145-152, 2014. Google Scholar
  16. S. Chen, M. Erwig, and E. Walkingshaw. An error-tolerant type system for variational lambda calculus. In ICFP, pages 29-40, 2012. Google Scholar
  17. S. Chen, M. Erwig, and E. Walkingshaw. Extending type inference to variational programs. TOPLAS, 36(1):1:1-1:54, 2014. Google Scholar
  18. S. Chen, M. Erwig, and E. Walkingshaw. A calculus for variational programming. Technical report, University of Louisiana at Lafayette and Oregon State University, 2016. URL: http://shengchen1.bitbucket.org/ws/TechReport/vpc.pdf.
  19. M. d'Amorim, S. Lauterburg, and D. Marinov. Delta execution for efficient state-space exploration of object-oriented programs. TSE, 34(5):597-613, 2008. Google Scholar
  20. W. De Groef, D. Devriese, N. Nikiforakis, and F. Piessens. FlowFox: A web browser with flexible and precise information flow control. In CCS, pages 748-759, 2012. Google Scholar
  21. D. Devriese and F. Piessens. Noninterference through secure multi-execution. In S&P, pages 109-124, 2010. Google Scholar
  22. M. Erwig, K. Ostermann, T. Rendel, and E. Walkingshaw. Adding configuration to the choice calculus. In VAMOS, pages 13:1-13:8, 2013. Google Scholar
  23. M. Erwig and E. Walkingshaw. The choice calculus: A representation for software variation. TOSEM, 21(1):6:1-6:27, 2011. Google Scholar
  24. M. Erwig and E. Walkingshaw. Variation programming with the choice calculus. In GTTSE, LNCS 7680, pages 55-100, 2013. Google Scholar
  25. R. Harper. Practical Foundations for Programming Languages (2ed). Cambridge University Press, New York, NY, USA, 2016. Google Scholar
  26. P. Hosek and C. Cadar. Safe software updates via multi-version execution. In ICSE, pages 612-621, 2013. Google Scholar
  27. O. Kammar, S. Lindley, and N. Oury. Handlers in action. In ICFP, pages 145-158, 2013. Google Scholar
  28. C. Kästner, S. Apel, T. Thüm, and G. Saake. Type checking annotation-based product lines. TOSEM, 21(3):14:1-14:39, 2012. Google Scholar
  29. C. Kästner, P. G. Giarrusso, T. Rendel, S. Erdweg, K. Ostermann, and T. Berger. Variability-aware parsing in the presence of lexical macros and conditional compilation. In OOPSLA, pages 805-824, 2011. Google Scholar
  30. C. Kästner, A. von Rhein, S. Erdweg, J. Pusch, S. Apel, T. Rendel, and K. Ostermann. Toward variability-aware testing. In FOSD, pages 1-8, 2012. Google Scholar
  31. C. H. P. Kim, S. Khurshid, and D. Batory. Shared execution for efficiently testing product lines. In ISSRE, pages 221-230, 2012. Google Scholar
  32. C. Kolbitsch, B. Livshits, B. Zorn, and C. Seifert. Rozzle: De-cloaking internet malware. In S&P, pages 443-457, 2012. Google Scholar
  33. J. Liebig, A. Janker, F. Garbe, S. Apel, and C. Lengauer. Morpheus: Variability-aware refactoring in the wild. In ICSE, pages 380-391, 2015. Google Scholar
  34. J. Liebig, A. von Rhein, C. Kästner, S. Apel, J. Dörre, and C. Lengauer. Scalable analysis of variable software. In ESEC/FSE, pages 81-91, 2013. Google Scholar
  35. M. Maurer and D. Brumley. TACHYON: Tandem execution for efficient live patch testing. In USENIX Security Symposium, pages 43-43, 2012. Google Scholar
  36. M. Mezini and K. Ostermann. Variability management with feature-oriented programming and aspects. SEN, 29(6):127-136, 2004. Google Scholar
  37. S. Nadi, T. Berger, C. Kästner, and K. Czarnecki. Mining configuration constraints: Static analyses and empirical results. In ICSE, pages 140-151, 2014. Google Scholar
  38. S. Nadi, T. Berger, C. Kästner, and K. Czarnecki. Where do configuration constraints stem from? An extraction approach and an empirical study. TSE, 2015. Google Scholar
  39. H. Nguyen, C. Kästner, and T. N. Nguyen. Exploring variability-aware execution for testing plugin-based web applications. In ICSE, pages 907-918, 2014. Google Scholar
  40. M. Odersky, M. Sulzmann, and M. Wehr. Type inference with constrained types. Theory and Practice of Object Systems, 5(1):35-55, 1999. Google Scholar
  41. G. Plotkin and J. Power. Adequacy for algebraic effects. In FoSSaCS, pages 1-24, 2001. Google Scholar
  42. I. Schaefer, L. Bettini, V. Bono, F. Damiani, and N. Tanzarella. Delta-oriented programming of software product lines. In Software Product Lines: Going Beyond, pages 77-91. 2010. Google Scholar
  43. Y. Su, M. Attariyan, and J. Flinn. AutoBash: Improving configuration management with operating system causality analysis. In SOSP, pages 237-250, 2007. Google Scholar
  44. M. Sulzmann. A general type inference framework for hindley/milner style systems. In FLOPS, pages 248-263, 2001. Google Scholar
  45. W. N. Sumner, T. Bao, X. Zhang, and S. Prabhakar. Coalescing executions for fast uncertainty analysis. In ICSE, pages 581-590, 2011. Google Scholar
  46. S. Thaker, D. Batory, D. Kitchin, and W. Cook. Safe composition of product lines. In GPCE, pages 95-104, 2007. Google Scholar
  47. T. Thüm, S. Apel, C. Kästner, I. Schaefer, and G. Saake. A classification and survey of analysis strategies for software product lines. CSUR, 47(1):6, 2014. Google Scholar
  48. E. Torlak and R. Bodik. A lightweight symbolic virtual machine for solver-aided host languages. In PLDI, pages 530-541, 2014. Google Scholar
  49. J. Tucek, W. Xiong, and Y. Zhou. Efficient online validation with delta execution. In ASPLOS, pages 193-204, 2009. Google Scholar
  50. E. Walkingshaw. The choice calculus: A formal language of variation. PhD thesis, Oregon State University, 2013. Google Scholar
  51. E. Walkingshaw and M. Erwig. A calculus for modeling and implementing variation. In GPCE, pages 132-140, 2012. Google Scholar
  52. E. Walkingshaw, C. Kästner, M. Erwig, S. Apel, and E. Bodden. Variational data structures: Exploring trade-offs in computing with variability. In Onward!, pages 213-226, 2014. Google Scholar
  53. E. Walkingshaw and K. Ostermann. Projectional editing of variational software. In GPCE, pages 29-38, 2014. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact