Changeset 3652


Ignore:
Timestamp:
Mar 14, 2017, 4:34:27 PM (11 days ago)
Author:
mulligan
Message:

more on biblio. finished now, i think...

Location:
Papers/jar-cerco-2017
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-cerco-2017/cerco.bib

    r3651 r3652  
    463463}
    464464
     465@inproceedings{DBLP:conf/sefm/BarthePS05,
     466  author    = {Gilles Barthe and
     467               Mariela Pavlova and
     468               Gerardo Schneider},
     469  title     = {Precise Analysis of Memory Consumption using Program Logics},
     470  booktitle = {Third {IEEE} International Conference on Software Engineering and
     471               Formal Methods {(SEFM} 2005), 7-9 September 2005, Koblenz, Germany},
     472  pages     = {86--95},
     473  year      = {2005},
     474  crossref  = {DBLP:conf/sefm/2005},
     475  url       = {http://dx.doi.org/10.1109/SEFM.2005.34},
     476  doi       = {10.1109/SEFM.2005.34},
     477  timestamp = {Fri, 29 May 2015 14:21:25 +0200},
     478  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/sefm/BarthePS05},
     479  bibsource = {dblp computer science bibliography, http://dblp.org}
     480}
     481
     482@Inbook{DalZilio2005,
     483author="Dal Zilio, Silvano
     484and Gascon, R{\'e}gis",
     485editor="Yi, Kwangkeun",
     486title="Resource Bound Certification for a Tail-Recursive Virtual Machine",
     487bookTitle="Programming Languages and Systems: Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005. Proceedings",
     488year="2005",
     489publisher="Springer Berlin Heidelberg",
     490address="Berlin, Heidelberg",
     491pages="247--263",
     492isbn="978-3-540-32247-4",
     493doi="10.1007/11575467_17",
     494url="http://dx.doi.org/10.1007/11575467_17"
     495}
     496
     497
     498@Inbook{Chander2005,
     499author="Chander, Ajay
     500and Espinosa, David
     501and Islam, Nayeem
     502and Lee, Peter
     503and Necula, George",
     504editor="Sagiv, Mooly",
     505title="Enforcing Resource Bounds via Static Verification of Dynamic Checks",
     506bookTitle="Programming Languages and Systems: 14th European Symposium on Programming, ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005. Proceedings",
     507year="2005",
     508publisher="Springer Berlin Heidelberg",
     509address="Berlin, Heidelberg",
     510pages="311--325",
     511isbn="978-3-540-31987-0",
     512doi="10.1007/978-3-540-31987-0_22",
     513url="http://dx.doi.org/10.1007/978-3-540-31987-0_22"
     514}
     515
     516
     517@Inbook{He2009,
     518author="He, Guanhua
     519and Qin, Shengchao
     520and Luo, Chenguang
     521and Chin, Wei-Ngan",
     522editor="Liu, Zhiming
     523and Ravn, Anders P.",
     524title="Memory Usage Verification Using Hip/Sleek",
     525bookTitle="Automated Technology for Verification and Analysis: 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings",
     526year="2009",
     527publisher="Springer Berlin Heidelberg",
     528address="Berlin, Heidelberg",
     529pages="166--181",
     530isbn="978-3-642-04761-9",
     531doi="10.1007/978-3-642-04761-9_14",
     532url="http://dx.doi.org/10.1007/978-3-642-04761-9_14"
     533}
     534
     535
     536@inproceedings{Chin:2008:AMR:1375634.1375656,
     537 author = {Chin, Wei-Ngan and Nguyen, Huu Hai and Popeea, Corneliu and Qin, Shengchao},
     538 title = {Analysing Memory Resource Bounds for Low-level Programs},
     539 booktitle = {Proceedings of the 7th International Symposium on Memory Management},
     540 series = {ISMM '08},
     541 year = {2008},
     542 isbn = {978-1-60558-134-7},
     543 location = {Tucson, AZ, USA},
     544 pages = {151--160},
     545 numpages = {10},
     546 url = {http://doi.acm.org/10.1145/1375634.1375656},
     547 doi = {10.1145/1375634.1375656},
     548 acmid = {1375656},
     549 publisher = {ACM},
     550 address = {New York, NY, USA},
     551 keywords = {fixpoint analysis, heap space analysis, low level programs, stack space analysis},
     552}
     553
     554
     555@inproceedings{speed-precise-and-efficient-static-estimation-of-program-computational-complexity-2,
     556author = {Gulwani, Sumit and Mehra, Krishna and Chilimbi, Trishul},
     557title = {SPEED: Precise and Efficient Static Estimation of Program Computational Complexity},
     558booktitle = {Principles of Programming Languages (POPL)},
     559year = {2009},
     560month = {January},
     561abstract = {
     562
     563This paper describes an inter-procedural technique for computing symbolic bounds on the number of statements a procedure executes in terms of its scalar inputs and user-defined quantitative functions of input data-structures. Such computational complexity bounds for even simple programs are usually disjunctive, non-linear, and involve numerical properties of heaps. We address the challenges of generating these bounds using two novel ideas. We introduce a proof methodology based on multiple counter instrumentation (each counter can be initialized and incremented at potentially multiple program locations) that allows a given linear invariant generation tool to compute linear bounds individually onthese counter variables. The bounds on these counters are then composed together to generate total bounds that are non-linear and disjunctive. We also give an algorithm for automating this proof methodology. Our algorithm generates complexity bounds that are usually precise not only in terms of the computational complexity,but also in terms of the constant factors. Next, we introduce the notion of user-defined quantitative functions that can be associated with abstract data-structures, e.g., length of a list, height of a tree, etc. We show how to compute bounds in terms of these quantitative functions using a linear invariant generation tool that has support for handling uninterpreted functions. We show application of this methodology to commonly used data-structures (namely lists, list of lists, trees, bit-vectors) using examples from Microsoft product code. We observe that a few quantitative functions for each data-structure are usually sufficient to allow generation of symbolic complexity bounds of a variety of loops that iterate over these data-structures, and that it is straightforward to define these quantitative functions. The combination of these techniques enables generation of precise computational complexity bounds for real-world examples (drawn from Microsoft product code and C++ STL library code) for some of which it is non-trivial to even prove termination. Such automatically generated bounds are very useful for early detection of egregious performance problems in large modular codebases that are constantly being changed by multiple developers who make heavy use of code written by others without a good understanding of their implementation complexity.
     564
     565
     566},
     567publisher = {Association for Computing Machinery, Inc.},
     568url = {https://www.microsoft.com/en-us/research/publication/speed-precise-and-efficient-static-estimation-of-program-computational-complexity-2/},
     569address = {},
     570pages = {},
     571journal = {},
     572volume = {},
     573chapter = {},
     574isbn = {},
     575}
     576
     577@article{DBLP:journals/jot/BrabermanGY06,
     578  author    = {V{\'{\i}}ctor A. Braberman and
     579               Diego Garbervetsky and
     580               Sergio Yovine},
     581  title     = {A Static Analysis for Synthesizing Parametric Specifications of Dynamic
     582               Memory Consumption},
     583  journal   = {Journal of Object Technology},
     584  volume    = {5},
     585  number    = {5},
     586  pages     = {31--58},
     587  year      = {2006},
     588  url       = {http://dx.doi.org/10.5381/jot.2006.5.5.a2},
     589  doi       = {10.5381/jot.2006.5.5.a2},
     590  timestamp = {Fri, 19 Nov 2010 11:56:11 +0100},
     591  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jot/BrabermanGY06},
     592  bibsource = {dblp computer science bibliography, http://dblp.org}
     593}
     594
     595@techreport { symbolic-prediction-2007,
     596  author = {V. Braberman and F. Fernandez and D. Garbervetsky and S. Yovine},
     597  title = {Symbolic Prediction of Dynamic-Memory Requirements},
     598  year = {2007},
     599  institute = {VeriMag},
     600  number = {TR-2007-11}
     601}
     602
     603@article {DLTC:DLTC280,
     604author = {Gödel, Von Kurt},
     605title = {\"{U}BER EINE BISHER NOCH NICHT BEN\"UTZTE ERWEITERUNG DES FINITEN STANDPUNKTES},
     606journal = {Dialectica},
     607volume = {12},
     608number = {3-4},
     609publisher = {Blackwell Publishing Ltd},
     610issn = {1746-8361},
     611url = {http://dx.doi.org/10.1111/j.1746-8361.1958.tb01464.x},
     612doi = {10.1111/j.1746-8361.1958.tb01464.x},
     613pages = {280--287},
     614year = {1958},
     615}
     616
     617
     618
     619@article{DBLP:journals/tocl/AspertiR02,
     620  author    = {Andrea Asperti and
     621               Luca Roversi},
     622  title     = {Intuitionistic Light Affine Logic},
     623  journal   = {{ACM} Trans. Comput. Log.},
     624  volume    = {3},
     625  number    = {1},
     626  pages     = {137--175},
     627  year      = {2002},
     628  url       = {http://doi.acm.org/10.1145/504077.504081},
     629  doi       = {10.1145/504077.504081},
     630  timestamp = {Fri, 21 Nov 2003 08:34:41 +0100},
     631  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/tocl/AspertiR02},
     632  bibsource = {dblp computer science bibliography, http://dblp.org}
     633}
     634
     635
     636@article{GIRARD19871,
     637title = "Linear logic",
     638journal = "Theoretical Computer Science",
     639volume = "50",
     640number = "1",
     641pages = "1 - 101",
     642year = "1987",
     643note = "",
     644issn = "0304-3975",
     645doi = "http://dx.doi.org/10.1016/0304-3975(87)90045-4",
     646url = "http://www.sciencedirect.com/science/article/pii/0304397587900454",
     647author = "Jean-Yves Girard",
     648
     649}
     650
     651@misc { mathematica,
     652  title = {Wolfram {Mathematica} website},
     653  url = {https://www.wolfram.com/mathematica/},
     654  note = {Accessed March 2017},
     655  year = {2017},
     656  key = {mathematica}
     657}
     658
    465659@Article{Albert2011,
    466660author="Albert, Elvira
  • Papers/jar-cerco-2017/conclusions.tex

    r3651 r3652  
    4646
    4747Many different approaches to resource analysis---asymptotic and concrete, working at low- and high-levels of abstraction---are present within the literature.
    48 We now survey these approaches.
     48We now survey these approaches, drawing a distinction between low-level approaches that operate directly on the object code (or bytecode) produced by a compiler, and approaches that operate at a higher-level of abstraction.
    4949
    5050\subsubsection{Object-code approaches}
     
    6969
    7070Abstract Interpretation may also be used to derive upper bounds for stack usage (e.g.~\cite{Regehr:2005:ESO:1113830.1113833}), and Abstract Interpretation tools for predicting stack space usage, for example the StackAnalyzer tool~\cite{stackanalyzer}, are also commercially available.
     71An Abstract Interpretation-based analysis of resource usage for bytecode programs of a stack-based virtual machine was presented in~\cite{DalZilio2005}.
     72
     73Program logics for analysing resource use of low-level code have also been investigated (similar program logics for high-level programs will be discussed below).
     74Barthe et al. developed a program logic for low-level Java bytecode programs, able to certify bounds on a bytecode program's heap usage~\cite{DBLP:conf/sefm/BarthePS05}.
    7175
    7276\paragraph{High-level approaches}
     
    8589Coupled with the KeY symbolic reasoning/automated reasoning system~\cite{KeYBook2016}, these assertions may be automatically verified, obtaining trustworthy upper bounds on a Java program's dynamic heap space usage at runtime.
    8690
    87 Other work has explored the use of Computer Algebra Software, such as the Mathematica system, for deriving closed-form upper-bounds of a program's resource usage~\cite{Albert2011}.
     91Similarly, the automatic instrumentation provided in~\cite{He2009}, combined with the Hip/SLEEK automated reasoning tool, can produce certified bounds on a program's memory usage.
     92This instrumentation is proven sound with respect to an operational semantics of the programming language considered.
    8893
    89 Previous works have researched various static analyses of time- and space-usage of programs written in a simple functional programming language with regions, called Safe~\cite{Montenegro2010,Montenegro2010a}.
     94Other work has explored the use of Computer Algebra Software, such as the Wolfram Mathematica system~\cite{mathematica}, for deriving closed-form upper-bounds of a program's resource usage~\cite{Albert2011}.
     95A high-level static analysis for synthesising non-linear bounds on the memory usage of programs written in a Java-like programming language, extended with regions, made use of Bernstein bases in~\cite{symbolic-prediction-2007,DBLP:journals/jot/BrabermanGY06}.
     96A series of work presented various static analyses of time- and space-usage of programs written in a simple functional programming language with regions, called Safe~\cite{Montenegro2010,Montenegro2010a}.
    9097One such analysis was verified in Isabelle/HOL~\cite{deDios2011}.
     98An intraprocedural approach for deriving symbolic bounds on the number of times statements in a procedure are executed, given as a function of the procedure's scalar inputs, was developed by Gulwani et al~\cite{speed-precise-and-efficient-static-estimation-of-program-computational-complexity-2}.
     99The intraprocedural analysis was implemented in the SPEED tool, and used to compute bounds for high-level programs, in several case studies.
     100Another analysis for producing symbolic bounds---this time on stack and heap usage---of embedded code written in C, or similar languages, was presented in~\cite{Chin:2008:AMR:1375634.1375656}.
     101
     102Resource bounds may also be checked dynamically, at run time, using automatically inserted instrumentation code.
     103This naturally incurs a runtime cost.
     104A hybrid static-dynamic checker of resource bounds, for a novel programming language specifically designed to ease the implementation of the technique, was explored in~\cite{Chander2005}.
    91105
    92106The use of types to bound, or program logics to reason about, a program's resource usage have also been extensively investigated in previous work.
     
    96110This approach was first pioneered by Hoffman and Jost for amortized, linear bounds on resource consumption~\cite{DBLP:conf/esop/HofmannJ06}, who focussed on predicting heap-space usage.
    97111Campbell also used a variant of this approach to predict stack space usage~\cite{bac-thesis08,bac-giveback08,bac-esop09}, whilst Atkey extended the approach to imperative languages~\cite{Atkey2010}, using ideas from Separation Logic~\cite{Reynolds:2002:SLL:645683.664578}.
    98 Recent work has extended this approach to include more features of the core programming language~\cite{Hoffmann2015}, improving the resource analysis~\cite{Hoffmann:2012:MAR:2362389.2362393}, and to apply extensions of the technique to case studies, demonstrating that cryptographic code is free from side-channel attacks~\cite{chan-ngo-verifying-2017}.
     112Recent work has extended this approach to include more features of the core programming language~\cite{Hoffmann2015}, improving the resource analysis~\cite{Hoffmann:2012:MAR:2362389.2362393}, and to apply extensions of the technique to case studies, for example in demonstrating that cryptographic code is free from side-channel attacks~\cite{chan-ngo-verifying-2017}.
    99113
    100114In related work, Salvucci and Chailloux~\cite{Salvucci201627} used a static type and effect system to bound runtime heap usage of an impure functional programming language, similar to ML.
     
    106120
    107121Implicit Computational Complexity represents another related approach to bounding resource usage via types~\cite{DalLago2012}.
    108 Here, a fragment of Linear Logic, or some other substructural logic, is taken as the language of types of some calculus, with a provable guarantee that typeable terms of the calculus normalise to a value in some bounded (e.g. polynomial in the size of the term) number of reduction steps.
     122Here, a fragment of Linear Logic~\cite{GIRARD19871}, or some other substructural logic, is taken as the language of types of some calculus, with a provable guarantee that typeable terms of the calculus normalise to a value in some bounded number of reduction steps (e.g. polynomial in the size of the term, as in the case of type systems inspired by Intuitionistic Light Affine Logic~\cite{DBLP:journals/tocl/AspertiR02}).
    109123Note that compared to the concrete complexity measures dealt with in this work, bounding reduction steps is rather coarse-grained: one reduction step in the calculus may decompose into some non-constant number of primitive machine operations, when executed on physical hardware.
    110124Indeed, the focus of Implicit Computational Complexity is not to capture \emph{concrete} resource usage of programs, but to provide a type-theoretic interpretation of complexity classes.
    111 A formalisation of a cost semantics for System T using ideas from Implicit Computational Complexity was formalised in Coq~\cite{Danner:2013:SCA:2428116.2428123}.
     125A formalisation of a cost semantics for System T~\cite{DLTC:DLTC280} using ideas from Implicit Computational Complexity was formalised in Coq~\cite{Danner:2013:SCA:2428116.2428123}.
    112126
    113127Several program logics for reasoning about a program's resource consumption have been investigated in the literature.
Note: See TracChangeset for help on using the changeset viewer.