Changeset 3651


Ignore:
Timestamp:
Mar 14, 2017, 11:14:29 AM (11 days ago)
Author:
mulligan
Message:

more work on conclusions and related work, bibliography growing to gigantic proportions

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

Legend:

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

    r3650 r3651  
    102102 address = {New York, NY, USA},
    103103 keywords = {CompCert, Compositional compiler verification, separate compilation},
     104}
     105
     106@Inbook{Atkey2010,
     107author="Atkey, Robert",
     108editor="Gordon, Andrew D.",
     109title="Amortised Resource Analysis with Separation Logic",
     110bookTitle="Programming Languages and Systems: 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings",
     111year="2010",
     112publisher="Springer Berlin Heidelberg",
     113address="Berlin, Heidelberg",
     114pages="85--103",
     115isbn="978-3-642-11957-6",
     116doi="10.1007/978-3-642-11957-6_6",
     117url="http://dx.doi.org/10.1007/978-3-642-11957-6_6"
     118}
     119
     120
     121@Inbook{Aspinall2010,
     122author="Aspinall, David
     123and Atkey, Robert
     124and MacKenzie, Kenneth
     125and Sannella, Donald",
     126editor="Wirsing, Martin
     127and Hofmann, Martin
     128and Rauschmayer, Axel",
     129title="Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode",
     130bookTitle="Trustworthly Global Computing: 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers",
     131year="2010",
     132publisher="Springer Berlin Heidelberg",
     133address="Berlin, Heidelberg",
     134pages="1--22",
     135isbn="978-3-642-15640-3",
     136doi="10.1007/978-3-642-15640-3_1",
     137url="http://dx.doi.org/10.1007/978-3-642-15640-3_1"
     138}
     139
     140
     141@article{Salvucci201627,
     142title = "Memory Consumption Analysis for a Functional and Imperative Language ",
     143journal = "Electronic Notes in Theoretical Computer Science ",
     144volume = "330",
     145number = "",
     146pages = "27 - 46",
     147year = "2016",
     148note = "\{RAC\} 2016 - Resource Aware Computing ",
     149issn = "1571-0661",
     150doi = "http://dx.doi.org/10.1016/j.entcs.2016.12.013",
     151url = "http://www.sciencedirect.com/science/article/pii/S1571066116301207",
     152author = "Jérémie Salvucci and Emmanuel Chailloux",
     153keywords = "ML",
     154keywords = "regions",
     155keywords = "static analysis",
     156keywords = "memory analysis ",
     157abstract = "Abstract The omnipresence of resource-constrained embedded systems makes them critical components. Programmers have to provide strong guarantees about their runtime behavior to make them reliable. Among these, giving an upper bound of live memory at runtime is mandatory to prevent heap overflows from happening. The paper proposes a semi-automatic technique to infer the space complexity of ML-like programs with explicit region management. It aims at combining existing formalisms to obtain the space complexity of imperative and purely functional programs in a consistent framework. "
     158}
     159
     160
     161@Inbook{Hoffmann2015,
     162author="Hoffmann, Jan
     163and Shao, Zhong",
     164editor="Vitek, Jan",
     165title="Automatic Static Cost Analysis for Parallel Programs",
     166bookTitle="Programming Languages and Systems: 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings",
     167year="2015",
     168publisher="Springer Berlin Heidelberg",
     169address="Berlin, Heidelberg",
     170pages="132--157",
     171isbn="978-3-662-46669-8",
     172doi="10.1007/978-3-662-46669-8_6",
     173url="http://dx.doi.org/10.1007/978-3-662-46669-8_6"
     174}
     175
     176
     177@inproceedings{HAH12,
     178  author    = {Jan Hoffmann and Klaus Aehlig and
     179               Martin Hofmann},
     180  title     = {{Resource Aware ML}},
     181  booktitle = {{24rd International Conference on Computer Aided
     182                  Verification (CAV'12)}},
     183  publisher = {Springer},
     184  series    = {Lecture Notes in Computer Science},
     185  volume    = {7358},
     186  pages     = {781-786},
     187  year      = {2012}
    104188}
    105189
     
    377461 address = {New York, NY, USA},
    378462 keywords = {compiler verification, interactive proof assistants},
    379 }
     463}
     464
     465@Article{Albert2011,
     466author="Albert, Elvira
     467and Arenas, Puri
     468and Genaim, Samir
     469and Puebla, Germ{\'a}n",
     470title="Closed-Form Upper Bounds in Static Cost Analysis",
     471journal="Journal of Automated Reasoning",
     472year="2011",
     473volume="46",
     474number="2",
     475pages="161--203",
     476abstract="The classical approach to automatic cost analysis consists of two phases. Given a program and some measure of cost, the analysis first produces cost relations (CRs), i.e., recursive equations which capture the cost of the program in terms of the size of its input data. Second, CRs are converted into closed-form, i.e., without recurrences. Whereas the first phase has received considerable attention, with a number of cost analyses available for a variety of programming languages, the second phase has been comparatively less studied. This article presents, to our knowledge, the first practical framework for the generation of closed-form upper bounds for CRs which (1) is fully automatic, (2) can handle the distinctive features of CRs, originating from cost analysis of realistic programming languages, (3) is not restricted to simple complexity classes, and (4) produces reasonably accurate solutions. A key idea in our approach is to view CRs as programs, which allows applying semantic-based static analyses and transformations to bound them, namely our method is based on the inference of ranking functions and loop invariants and on the use of partial evaluation.",
     477issn="1573-0670",
     478doi="10.1007/s10817-010-9174-1",
     479url="http://dx.doi.org/10.1007/s10817-010-9174-1"
     480}
     481
     482
     483@article{ALBERT200767,
     484title = "Experiments in Cost Analysis of Java Bytecode",
     485journal = "Electronic Notes in Theoretical Computer Science",
     486volume = "190",
     487number = "1",
     488pages = "67 - 83",
     489year = "2007",
     490note = "",
     491issn = "1571-0661",
     492doi = "http://dx.doi.org/10.1016/j.entcs.2007.02.061",
     493url = "http://www.sciencedirect.com/science/article/pii/S1571066107005294",
     494author = "E. Albert and P. Arenas and S. Genaim and G. Puebla and D. Zanardini",
     495keywords = "Cost analysis",
     496keywords = "Java bytecode",
     497keywords = "cost relations",
     498keywords = "recurrence equations",
     499keywords = "complexity"
     500}
    380501
    381502@article{Wang:2014:CVM:2714064.2660201,
     
    598719  doi = {10.1007/978-3-642-00590-9_14}
    599720}
     721
     722@Inbook{Chalin2006,
     723author="Chalin, Patrice
     724and Kiniry, Joseph R.
     725and Leavens, Gary T.
     726and Poll, Erik",
     727editor="de Boer, Frank S.
     728and Bonsangue, Marcello M.
     729and Graf, Susanne
     730and de Roever, Willem-Paul",
     731title="Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2",
     732bookTitle="Formal Methods for Components and Objects: 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures",
     733year="2006",
     734publisher="Springer Berlin Heidelberg",
     735address="Berlin, Heidelberg",
     736pages="342--363",
     737isbn="978-3-540-36750-5",
     738doi="10.1007/11804192_16",
     739url="http://dx.doi.org/10.1007/11804192_16"
     740}
     741
     742
     743@book{KeYBook2016,
     744title = {Deductive Software Verification - The KeY Book - From Theory to Practice},
     745editor = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H{\"{a}}hnle and Peter H. Schmitt and Mattias Ulbrich},
     746url = {http://dx.doi.org/10.1007/978-3-319-49812-6},
     747doi = {10.1007/978-3-319-49812-6},
     748isbn = {978-3-319-49811-9},
     749year = {2016},
     750date = {2016-12-16},
     751volume = {10001},
     752publisher = {Springer},
     753series = {Lecture Notes in Computer Science},
     754keywords = {},
     755pubstate = {published},
     756tppubtype = {book}
     757}
     758
     759
     760
     761@Inbook{Montenegro2010a,
     762author="Montenegro, Manuel
     763and Pe{\~{n}}a, Ricardo
     764and Segura, Clara",
     765editor="van Eekelen, Marko
     766and Shkaravska, Olha",
     767title="A Space Consumption Analysis by Abstract Interpretation",
     768bookTitle="Foundational and Practical Aspects of Resource Analysis: First International Workshop, FOPARA 2009, Eindhoven, The Netherlands, November 6, 2009, Revised Selected Papers",
     769year="2010",
     770publisher="Springer Berlin Heidelberg",
     771address="Berlin, Heidelberg",
     772pages="34--50",
     773isbn="978-3-642-15331-0",
     774doi="10.1007/978-3-642-15331-0_3",
     775url="http://dx.doi.org/10.1007/978-3-642-15331-0_3"
     776}
     777
     778
     779@Inbook{Montenegro2010,
     780author="Montenegro, Manuel
     781and Pe{\~{n}}a, Ricardo
     782and Segura, Clara",
     783editor="Escobar, Santiago",
     784title="A Simple Region Inference Algorithm for a First-Order Functional Language",
     785bookTitle="Functional and Constraint Logic Programming: 18th International Workshop, WFLP 2009, Brasilia, Brazil, June 28, 2009, Revised Selected Papers",
     786year="2010",
     787publisher="Springer Berlin Heidelberg",
     788address="Berlin, Heidelberg",
     789pages="145--161",
     790isbn="978-3-642-11999-6",
     791doi="10.1007/978-3-642-11999-6_10",
     792url="http://dx.doi.org/10.1007/978-3-642-11999-6_10"
     793}
     794
     795
     796@Inbook{deDios2011,
     797author="de Dios, Javier
     798and Pe{\~{n}}a, Ricardo",
     799editor="Butler, Michael
     800and Schulte, Wolfram",
     801title="Certification of Safe Polynomial Memory Bounds",
     802bookTitle="FM 2011: Formal Methods: 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings",
     803year="2011",
     804publisher="Springer Berlin Heidelberg",
     805address="Berlin, Heidelberg",
     806pages="184--199",
     807isbn="978-3-642-21437-0",
     808doi="10.1007/978-3-642-21437-0_16",
     809url="http://dx.doi.org/10.1007/978-3-642-21437-0_16"
     810}
     811
     812
     813@Inbook{Albert2012,
     814author="Albert, Elvira
     815and Bubel, Richard
     816and Genaim, Samir
     817and H{\"a}hnle, Reiner
     818and Rom{\'a}n-D{\'i}ez, Guillermo",
     819editor="de Lara, Juan
     820and Zisman, Andrea",
     821title="Verified Resource Guarantees for Heap Manipulating Programs",
     822bookTitle="Fundamental Approaches to Software Engineering: 15th International Conference, FASE 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings",
     823year="2012",
     824publisher="Springer Berlin Heidelberg",
     825address="Berlin, Heidelberg",
     826pages="130--145",
     827isbn="978-3-642-28872-2",
     828doi="10.1007/978-3-642-28872-2_10",
     829url="http://dx.doi.org/10.1007/978-3-642-28872-2_10"
     830}
     831
     832
     833@Inbook{Nipkow2015,
     834author="Nipkow, Tobias",
     835editor="Urban, Christian
     836and Zhang, Xingyuan",
     837title="Amortized Complexity Verified",
     838bookTitle="Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings",
     839year="2015",
     840publisher="Springer International Publishing",
     841address="Cham",
     842pages="310--324",
     843isbn="978-3-319-22102-1",
     844doi="10.1007/978-3-319-22102-1_21",
     845url="http://dx.doi.org/10.1007/978-3-319-22102-1_21"
     846}
     847
     848
     849@article{Hoffmann:2012:MAR:2362389.2362393,
     850 author = {Hoffmann, Jan and Aehlig, Klaus and Hofmann, Martin},
     851 title = {Multivariate Amortized Resource Analysis},
     852 journal = {ACM Trans. Program. Lang. Syst.},
     853 issue_date = {October 2012},
     854 volume = {34},
     855 number = {3},
     856 month = nov,
     857 year = {2012},
     858 issn = {0164-0925},
     859 pages = {14:1--14:62},
     860 articleno = {14},
     861 numpages = {62},
     862 url = {http://doi.acm.org/10.1145/2362389.2362393},
     863 doi = {10.1145/2362389.2362393},
     864 acmid = {2362393},
     865 publisher = {ACM},
     866 address = {New York, NY, USA},
     867 keywords = {Amortized analysis, functional programming, quantitative analysis, resource consumption, static analysis},
     868}
     869
     870
     871
     872@Inbook{Chargueraud2015,
     873author="Chargu{\'e}raud, Arthur
     874and Pottier, Fran{\c{c}}ois",
     875editor="Urban, Christian
     876and Zhang, Xingyuan",
     877title="Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation",
     878bookTitle="Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings",
     879year="2015",
     880publisher="Springer International Publishing",
     881address="Cham",
     882pages="137--153",
     883isbn="978-3-319-22102-1",
     884doi="10.1007/978-3-319-22102-1_9",
     885url="http://dx.doi.org/10.1007/978-3-319-22102-1_9"
     886}
     887
     888
     889@Inbook{Teller2002,
     890author="Teller, David
     891and Zimmer, Pascal
     892and Hirschkoff, Daniel",
     893editor="Brim, Lubo{\v{s}}
     894and K{\v{r}}et{\'i}nsk{\'y}, Mojm{\'i}r
     895and Ku{\v{c}}era, Anton{\'i}n
     896and Jan{\v{c}}ar, Petr",
     897title="Using Ambients to Control Resources*                  ",
     898bookTitle="CONCUR 2002 --- Concurrency Theory: 13th International Conference Brno, Czech Republic, August 20--23, 2002 Proceedings",
     899year="2002",
     900publisher="Springer Berlin Heidelberg",
     901address="Berlin, Heidelberg",
     902pages="288--303",
     903isbn="978-3-540-45694-0",
     904doi="10.1007/3-540-45694-5_20",
     905url="http://dx.doi.org/10.1007/3-540-45694-5_20"
     906}
     907
     908
     909@article{DBLP:journals/jfp/0002S15,
     910  author    = {Jan Hoffmann and
     911               Zhong Shao},
     912  title     = {Type-based amortized resource analysis with integers and arrays},
     913  journal   = {J. Funct. Program.},
     914  volume    = {25},
     915  year      = {2015},
     916  url       = {http://dx.doi.org/10.1017/S0956796815000192},
     917  doi       = {10.1017/S0956796815000192},
     918  timestamp = {Tue, 26 Jan 2016 16:08:20 +0100},
     919  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jfp/0002S15},
     920  bibsource = {dblp computer science bibliography, http://dblp.org}
     921}
     922
     923@Inbook{Barbanera2003,
     924author="Barbanera, Franco
     925and Bugliesi, Michele
     926and Dezani-Ciancaglini, Mariangiola
     927and Sassone, Vladimiro",
     928editor="Saraswat, Vijay A.",
     929title="A Calculus of Bounded Capacities",
     930bookTitle="Advances in Computing Science -- ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation: 8th Asian Computing Science Conference, Mumbai, India, December 10-12, 2003. Proceedings",
     931year="2003",
     932publisher="Springer Berlin Heidelberg",
     933address="Berlin, Heidelberg",
     934pages="205--223",
     935isbn="978-3-540-40965-6",
     936doi="10.1007/978-3-540-40965-6_14",
     937url="http://dx.doi.org/10.1007/978-3-540-40965-6_14"
     938}
     939
     940@article{Danielsson:2008:LST:1328897.1328457,
     941 author = {Danielsson, Nils Anders},
     942 title = {Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures},
     943 journal = {SIGPLAN Not.},
     944 issue_date = {January 2008},
     945 volume = {43},
     946 number = {1},
     947 month = jan,
     948 year = {2008},
     949 issn = {0362-1340},
     950 pages = {133--144},
     951 numpages = {12},
     952 url = {http://doi.acm.org/10.1145/1328897.1328457},
     953 doi = {10.1145/1328897.1328457},
     954 acmid = {1328457},
     955 publisher = {ACM},
     956 address = {New York, NY, USA},
     957 keywords = {amortised time complexity, dependent types, lazy evaluation, purely functional data structures},
     958}
     959
     960
     961@inproceedings{Crary:2000:RBC:325694.325716,
     962 author = {Crary, Karl and Weirich, Stephnie},
     963 title = {Resource Bound Certification},
     964 booktitle = {Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
     965 series = {POPL '00},
     966 year = {2000},
     967 isbn = {1-58113-125-9},
     968 location = {Boston, MA, USA},
     969 pages = {184--198},
     970 numpages = {15},
     971 url = {http://doi.acm.org/10.1145/325694.325716},
     972 doi = {10.1145/325694.325716},
     973 acmid = {325716},
     974 publisher = {ACM},
     975 address = {New York, NY, USA},
     976}
     977
     978@Inbook{McCarthy2016,
     979author="McCarthy, Jay
     980and Fetscher, Burke
     981and New, Max
     982and Feltey, Daniel
     983and Findler, Robert Bruce",
     984editor="Kiselyov, Oleg
     985and King, Andy",
     986title="A Coq Library for Internal Verification of Running-Times",
     987bookTitle="Functional and Logic Programming: 13th International Symposium, FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings",
     988year="2016",
     989publisher="Springer International Publishing",
     990address="Cham",
     991pages="144--162",
     992isbn="978-3-319-29604-3",
     993doi="10.1007/978-3-319-29604-3_10",
     994url="http://dx.doi.org/10.1007/978-3-319-29604-3_10"
     995}
     996
     997@inproceedings { chan-ngo-verifying-2017,
     998  title = {Verifying and Synthesizing Constant-Resource Implementations with Types},
     999  author = {Van Chan Ngo and Mario Dehesa-Azuara and Matthew Fredrikson and Jan Hoffmann},
     1000  booktitle = {Proceedings of the {IEEE} Symposium on Security and Privacy},
     1001  year = {2017},
     1002  note = {to appear}
     1003}
     1004
     1005@Inbook{Brady2006,
     1006author="Brady, Edwin
     1007and Hammond, Kevin",
     1008editor="Butterfield, Andrew
     1009and Grelck, Clemens
     1010and Huch, Frank",
     1011title="A Dependently Typed Framework for Static Analysis of Program Execution Costs",
     1012bookTitle="Implementation and Application of Functional Languages: 17th International Workshop, IFL 2005, Dublin, Ireland, September 19-21, 2005, Revised Selected Papers",
     1013year="2006",
     1014publisher="Springer Berlin Heidelberg",
     1015address="Berlin, Heidelberg",
     1016pages="74--90",
     1017isbn="978-3-540-69175-4",
     1018doi="10.1007/11964681_5",
     1019url="http://dx.doi.org/10.1007/11964681_5"
     1020}
     1021
     1022
     1023@inproceedings{Danner:2013:SCA:2428116.2428123,
     1024 author = {Danner, Norman and Paykin, Jennifer and Royer, James S.},
     1025 title = {A Static Cost Analysis for a Higher-order Language},
     1026 booktitle = {Proceedings of the 7th Workshop on Programming Languages Meets Program Verification},
     1027 series = {PLPV '13},
     1028 year = {2013},
     1029 isbn = {978-1-4503-1860-0},
     1030 location = {Rome, Italy},
     1031 pages = {25--34},
     1032 numpages = {10},
     1033 url = {http://doi.acm.org/10.1145/2428116.2428123},
     1034 doi = {10.1145/2428116.2428123},
     1035 acmid = {2428123},
     1036 publisher = {ACM},
     1037 address = {New York, NY, USA},
     1038 keywords = {automated theorem proving, certified bounds, higher-order complexity},
     1039}
     1040
     1041
     1042@inproceedings{Reynolds:2002:SLL:645683.664578,
     1043 author = {Reynolds, John C.},
     1044 title = {Separation Logic: A Logic for Shared Mutable Data Structures},
     1045 booktitle = {Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science},
     1046 series = {LICS '02},
     1047 year = {2002},
     1048 isbn = {0-7695-1483-9},
     1049 pages = {55--74},
     1050 numpages = {20},
     1051 url = {http://dl.acm.org/citation.cfm?id=645683.664578},
     1052 acmid = {664578},
     1053 publisher = {IEEE Computer Society},
     1054 address = {Washington, DC, USA},
     1055}
    6001056
    6011057@article{ASPINALL2007411,
  • Papers/jar-cerco-2017/conclusions.tex

    r3650 r3651  
    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.
    7171
    72 \paragraph{Type- and program logic-based analyses}
     72\paragraph{High-level approaches}
    7373
    74 Resource Aware ML (RAML) is a first-order statically typed functional programming language~\cite{Hoffmann11,HAH12Toplas,HoffHof10}.
    75 The RAML type system is able to derive polynomial resource bounds from first-order functional programs, using a variant of the `potential method'.
    76 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 heap-space usage.
    77 Campbell also used a variant of this approach to predict stack space usage~\cite{bac-thesis08,bac-giveback08,bac-esop09}.
    78 
    79 Implicit Computational Complexity represents another related approach to bounding resource usage via types~\cite{DalLago2012}.
    80 Here, a fragment of Linear Logic, or some other substructural logic, is taken as the type-language of a programming language, with a provable guarantee that typeable terms normalise to a value in some bounded (e.g. polynomial in the size of the term) number of reduction steps.
    81 Note that complained 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.
    82 Indeed, 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.
    83 
    84 Several program logics for reasoning about a program's resource consumption have been investigated in the literature.
    85 
    86 Aspinall et al. developed a program logic for a subset of the Java Virtual Machine's instruction set, capable of establishing resource bounds on JVM programs~\cite{ASPINALL2007411}.
    87 The soundness of the logic was formally verified in Isabelle/HOL.
    88 Along similar lines, Carbonneaux et al. developed a `quantitative Hoare logic' for reasoning about stack space usage of CompCert C programs~\cite{DBLP:conf/pldi/Carbonneaux0RS14}.
    89 The soundness of the logic was also formally verified, using the Coq proof assistant.
    90 This work will be further discussed below.
    91 
    92 \subsubsection{High-level approaches}
    93 
    94 \paragraph{Compiler-based cost-model lifting}
    95 Perhaps the most similar piece of work to our own is the recent work by Carbonneaux \emph{et al}~\cite{DBLP:conf/pldi/Carbonneaux0RS14}, who extended the CompCert verified C compiler in order to lift a concrete cost model for stack space usage back to the C source-level.
     74Perhaps the most closely related piece of work to our own is the recent work by Carbonneaux \emph{et al}~\cite{DBLP:conf/pldi/Carbonneaux0RS14}, who extended the CompCert verified C compiler in order to lift a concrete cost model for stack space usage back to the C source-level.
    9675Like CerCo, this work was verified within a theorem prover---in this case Coq, rather than Matita.
    9776Though Carbonneaux \emph{et al} were working entirely independently of the project described herein\footnote{Personal communication with Carbonneaux and Hoffmann}, the two pieces of work share some remarkable similarities, with both projects developing an analogue of the `structured trace' data structure described earlier in this paper in order to facilitate the verification of the lifting.
     
    10180Carbonneaux \emph{at al} lift their model from the assembly generated by the CompCert compiler; we must go further, to the level of machine code, in order to lift our timing cost model, necessitating the development of a verified assembler.
    10281Nevertheless, despite these differences, the two projects are clearly closely related.
     82
     83Another closely related piece of work to our own is COSTA~\cite{Albert2012}, a heap resource bound static analysis system for the Java programming language, building on previous work investigating cost models for Java bytecode programs~\cite{ALBERT200767}.
     84COSTA is able to produce parametric heap resource bounds for a given Java program, which are made manifest as Java Modelling Language (JML)~\cite{Chalin2006} assertions, inserted into the Java source file.
     85Coupled 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
     87Other 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}.
     88
     89Previous 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}.
     90One such analysis was verified in Isabelle/HOL~\cite{deDios2011}.
     91
     92The use of types to bound, or program logics to reason about, a program's resource usage have also been extensively investigated in previous work.
     93
     94Resource Aware ML (RAML) is a first-order statically typed functional programming language~\cite{Hoffmann11,HAH12Toplas,HoffHof10,HAH12,DBLP:journals/jfp/0002S15}.
     95The RAML type system is able to derive polynomial resource bounds from first-order functional programs, using a variant of the `potential method'.
     96This 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.
     97Campbell 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}.
     98Recent 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}.
     99
     100In 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.
     101Domain-specific type systems and calculi of mobile processes, for bounding agents in a distributed setting, have also been investigated~\cite{Barbanera2003,Teller2002}.
     102Brady and Hammond also investigated a dependent type system extended with features for bounding a program's dynamic resource usage~\cite{Brady2006}.
     103Similar ideas had previously been investigated by Crary and Weirich~\cite{Crary:2000:RBC:325694.325716}.
     104Libraries within dependently-typed languages, such as Coq~\cite{McCarthy2016} and Agda~\cite{Danielsson:2008:LST:1328897.1328457}, have also been written for reasoning about the complexity of algorithms written in the language.
     105One-off machine-checked verifications of the algorithmic complexity of various data structure implementations, and operations over them, have also been investigated (e.g.~\cite{Chargueraud2015,Nipkow2015}).
     106
     107Implicit Computational Complexity represents another related approach to bounding resource usage via types~\cite{DalLago2012}.
     108Here, 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.
     109Note 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.
     110Indeed, 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.
     111A formalisation of a cost semantics for System T using ideas from Implicit Computational Complexity was formalised in Coq~\cite{Danner:2013:SCA:2428116.2428123}.
     112
     113Several program logics for reasoning about a program's resource consumption have been investigated in the literature.
     114
     115Aspinall et al. developed a program logic for a subset of the Java Virtual Machine's instruction set, capable of establishing resource bounds on JVM programs~\cite{ASPINALL2007411}, similar in spirit to the `quantitative Hoare logic' mentioned above.
     116The soundness of the logic was formally verified in Isabelle/HOL.
     117Another program logic for reasoning about Java resource usage, based on ideas taken from Separation Logic, was also developed by Aspinall et al.~\cite{Aspinall2010}.
    103118
    104119\paragraph{Verified compilation}
Note: See TracChangeset for help on using the changeset viewer.