Changeset 3652
 Timestamp:
 Mar 14, 2017, 4:34:27 PM (6 weeks ago)
 Location:
 Papers/jarcerco2017
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Papers/jarcerco2017/cerco.bib
r3651 r3652 463 463 } 464 464 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), 79 September 2005, Koblenz, Germany}, 472 pages = {8695}, 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.unitrier.de/rec/bib/conf/sefm/BarthePS05}, 479 bibsource = {dblp computer science bibliography, http://dblp.org} 480 } 481 482 @Inbook{DalZilio2005, 483 author="Dal Zilio, Silvano 484 and Gascon, R{\'e}gis", 485 editor="Yi, Kwangkeun", 486 title="Resource Bound Certification for a TailRecursive Virtual Machine", 487 bookTitle="Programming Languages and Systems: Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 25, 2005. Proceedings", 488 year="2005", 489 publisher="Springer Berlin Heidelberg", 490 address="Berlin, Heidelberg", 491 pages="247263", 492 isbn="9783540322474", 493 doi="10.1007/11575467_17", 494 url="http://dx.doi.org/10.1007/11575467_17" 495 } 496 497 498 @Inbook{Chander2005, 499 author="Chander, Ajay 500 and Espinosa, David 501 and Islam, Nayeem 502 and Lee, Peter 503 and Necula, George", 504 editor="Sagiv, Mooly", 505 title="Enforcing Resource Bounds via Static Verification of Dynamic Checks", 506 bookTitle="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 48, 2005. Proceedings", 507 year="2005", 508 publisher="Springer Berlin Heidelberg", 509 address="Berlin, Heidelberg", 510 pages="311325", 511 isbn="9783540319870", 512 doi="10.1007/9783540319870_22", 513 url="http://dx.doi.org/10.1007/9783540319870_22" 514 } 515 516 517 @Inbook{He2009, 518 author="He, Guanhua 519 and Qin, Shengchao 520 and Luo, Chenguang 521 and Chin, WeiNgan", 522 editor="Liu, Zhiming 523 and Ravn, Anders P.", 524 title="Memory Usage Verification Using Hip/Sleek", 525 bookTitle="Automated Technology for Verification and Analysis: 7th International Symposium, ATVA 2009, Macao, China, October 1416, 2009. Proceedings", 526 year="2009", 527 publisher="Springer Berlin Heidelberg", 528 address="Berlin, Heidelberg", 529 pages="166181", 530 isbn="9783642047619", 531 doi="10.1007/9783642047619_14", 532 url="http://dx.doi.org/10.1007/9783642047619_14" 533 } 534 535 536 @inproceedings{Chin:2008:AMR:1375634.1375656, 537 author = {Chin, WeiNgan and Nguyen, Huu Hai and Popeea, Corneliu and Qin, Shengchao}, 538 title = {Analysing Memory Resource Bounds for Lowlevel Programs}, 539 booktitle = {Proceedings of the 7th International Symposium on Memory Management}, 540 series = {ISMM '08}, 541 year = {2008}, 542 isbn = {9781605581347}, 543 location = {Tucson, AZ, USA}, 544 pages = {151160}, 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{speedpreciseandefficientstaticestimationofprogramcomputationalcomplexity2, 556 author = {Gulwani, Sumit and Mehra, Krishna and Chilimbi, Trishul}, 557 title = {SPEED: Precise and Efficient Static Estimation of Program Computational Complexity}, 558 booktitle = {Principles of Programming Languages (POPL)}, 559 year = {2009}, 560 month = {January}, 561 abstract = { 562 563 This paper describes an interprocedural technique for computing symbolic bounds on the number of statements a procedure executes in terms of its scalar inputs and userdefined quantitative functions of input datastructures. Such computational complexity bounds for even simple programs are usually disjunctive, nonlinear, 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 nonlinear 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 userdefined quantitative functions that can be associated with abstract datastructures, 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 datastructures (namely lists, list of lists, trees, bitvectors) using examples from Microsoft product code. We observe that a few quantitative functions for each datastructure are usually sufficient to allow generation of symbolic complexity bounds of a variety of loops that iterate over these datastructures, and that it is straightforward to define these quantitative functions. The combination of these techniques enables generation of precise computational complexity bounds for realworld examples (drawn from Microsoft product code and C++ STL library code) for some of which it is nontrivial 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 }, 567 publisher = {Association for Computing Machinery, Inc.}, 568 url = {https://www.microsoft.com/enus/research/publication/speedpreciseandefficientstaticestimationofprogramcomputationalcomplexity2/}, 569 address = {}, 570 pages = {}, 571 journal = {}, 572 volume = {}, 573 chapter = {}, 574 isbn = {}, 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 = {3158}, 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.unitrier.de/rec/bib/journals/jot/BrabermanGY06}, 592 bibsource = {dblp computer science bibliography, http://dblp.org} 593 } 594 595 @techreport { symbolicprediction2007, 596 author = {V. Braberman and F. Fernandez and D. Garbervetsky and S. Yovine}, 597 title = {Symbolic Prediction of DynamicMemory Requirements}, 598 year = {2007}, 599 institute = {VeriMag}, 600 number = {TR200711} 601 } 602 603 @article {DLTC:DLTC280, 604 author = {Gödel, Von Kurt}, 605 title = {\"{U}BER EINE BISHER NOCH NICHT BEN\"UTZTE ERWEITERUNG DES FINITEN STANDPUNKTES}, 606 journal = {Dialectica}, 607 volume = {12}, 608 number = {34}, 609 publisher = {Blackwell Publishing Ltd}, 610 issn = {17468361}, 611 url = {http://dx.doi.org/10.1111/j.17468361.1958.tb01464.x}, 612 doi = {10.1111/j.17468361.1958.tb01464.x}, 613 pages = {280287}, 614 year = {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 = {137175}, 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.unitrier.de/rec/bib/journals/tocl/AspertiR02}, 632 bibsource = {dblp computer science bibliography, http://dblp.org} 633 } 634 635 636 @article{GIRARD19871, 637 title = "Linear logic", 638 journal = "Theoretical Computer Science", 639 volume = "50", 640 number = "1", 641 pages = "1  101", 642 year = "1987", 643 note = "", 644 issn = "03043975", 645 doi = "http://dx.doi.org/10.1016/03043975(87)900454", 646 url = "http://www.sciencedirect.com/science/article/pii/0304397587900454", 647 author = "JeanYves 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 465 659 @Article{Albert2011, 466 660 author="Albert, Elvira 
Papers/jarcerco2017/conclusions.tex
r3651 r3652 46 46 47 47 Many different approaches to resource analysisasymptotic and concrete, working at low and highlevels of abstractionare present within the literature. 48 We now survey these approaches .48 We now survey these approaches, drawing a distinction between lowlevel approaches that operate directly on the object code (or bytecode) produced by a compiler, and approaches that operate at a higherlevel of abstraction. 49 49 50 50 \subsubsection{Objectcode approaches} … … 69 69 70 70 Abstract 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. 71 An Abstract Interpretationbased analysis of resource usage for bytecode programs of a stackbased virtual machine was presented in~\cite{DalZilio2005}. 72 73 Program logics for analysing resource use of lowlevel code have also been investigated (similar program logics for highlevel programs will be discussed below). 74 Barthe et al. developed a program logic for lowlevel Java bytecode programs, able to certify bounds on a bytecode program's heap usage~\cite{DBLP:conf/sefm/BarthePS05}. 71 75 72 76 \paragraph{Highlevel approaches} … … 85 89 Coupled 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. 86 90 87 Other work has explored the use of Computer Algebra Software, such as the Mathematica system, for deriving closedform upperbounds of a program's resource usage~\cite{Albert2011}. 91 Similarly, 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. 92 This instrumentation is proven sound with respect to an operational semantics of the programming language considered. 88 93 89 Previous works have researched various static analyses of time and spaceusage of programs written in a simple functional programming language with regions, called Safe~\cite{Montenegro2010,Montenegro2010a}. 94 Other work has explored the use of Computer Algebra Software, such as the Wolfram Mathematica system~\cite{mathematica}, for deriving closedform upperbounds of a program's resource usage~\cite{Albert2011}. 95 A highlevel static analysis for synthesising nonlinear bounds on the memory usage of programs written in a Javalike programming language, extended with regions, made use of Bernstein bases in~\cite{symbolicprediction2007,DBLP:journals/jot/BrabermanGY06}. 96 A series of work presented various static analyses of time and spaceusage of programs written in a simple functional programming language with regions, called Safe~\cite{Montenegro2010,Montenegro2010a}. 90 97 One such analysis was verified in Isabelle/HOL~\cite{deDios2011}. 98 An 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{speedpreciseandefficientstaticestimationofprogramcomputationalcomplexity2}. 99 The intraprocedural analysis was implemented in the SPEED tool, and used to compute bounds for highlevel programs, in several case studies. 100 Another analysis for producing symbolic boundsthis time on stack and heap usageof embedded code written in C, or similar languages, was presented in~\cite{Chin:2008:AMR:1375634.1375656}. 101 102 Resource bounds may also be checked dynamically, at run time, using automatically inserted instrumentation code. 103 This naturally incurs a runtime cost. 104 A hybrid staticdynamic checker of resource bounds, for a novel programming language specifically designed to ease the implementation of the technique, was explored in~\cite{Chander2005}. 91 105 92 106 The use of types to bound, or program logics to reason about, a program's resource usage have also been extensively investigated in previous work. … … 96 110 This approach was first pioneered by Hoffman and Jost for amortized, linear bounds on resource consumption~\cite{DBLP:conf/esop/HofmannJ06}, who focussed on predicting heapspace usage. 97 111 Campbell also used a variant of this approach to predict stack space usage~\cite{bacthesis08,bacgiveback08,bacesop09}, 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 sidechannel attacks~\cite{channgoverifying2017}.112 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, for example in demonstrating that cryptographic code is free from sidechannel attacks~\cite{channgoverifying2017}. 99 113 100 114 In 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. … … 106 120 107 121 Implicit 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.122 Here, 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}). 109 123 Note that compared to the concrete complexity measures dealt with in this work, bounding reduction steps is rather coarsegrained: one reduction step in the calculus may decompose into some nonconstant number of primitive machine operations, when executed on physical hardware. 110 124 Indeed, the focus of Implicit Computational Complexity is not to capture \emph{concrete} resource usage of programs, but to provide a typetheoretic 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}.125 A 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}. 112 126 113 127 Several 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.