Changeset 3648


Ignore:
Timestamp:
Mar 13, 2017, 12:48:41 PM (7 months ago)
Author:
mulligan
Message:

exhausted my knowledge of type- and logic- based approaches to resource reasoning...

more citations, etc. etc.

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

Legend:

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

    r3647 r3648  
    3131  key = {stackanalyzer}
    3232}
     33
     34@phdthesis{Hoffmann11,
     35  author = {Jan Hoffmann},
     36  title = {{Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis}},
     37  school = {Ludwig-Maximilians-Universi{\"a}t M{\"u}nchen},
     38  year =  2011
     39}
     40
     41
    3342
    3443@article{Regehr:2005:ESO:1113830.1113833,
     
    5059 address = {New York, NY, USA},
    5160 keywords = {Microcontroller, abstract interpretation, call stack, context sensitive, dataflow analysis, interrupt-driven, sensor network},
     61}
     62
     63@inproceedings{DBLP:conf/esop/HofmannJ06,
     64  author    = {Martin Hofmann and
     65               Steffen Jost},
     66  title     = {Type-Based Amortised Heap-Space Analysis},
     67  booktitle = {Programming Languages and Systems, 15th European Symposium on Programming,
     68               {ESOP} 2006, Held as Part of the Joint European Conferences on Theory
     69               and Practice of Software, {ETAPS} 2006, Vienna, Austria, March 27-28,
     70               2006, Proceedings},
     71  pages     = {22--37},
     72  year      = {2006},
     73  crossref  = {DBLP:conf/esop/2006},
     74  url       = {http://dx.doi.org/10.1007/11693024_3},
     75  doi       = {10.1007/11693024_3},
     76  timestamp = {Thu, 28 May 2015 17:23:23 +0200},
     77  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/esop/HofmannJ06},
     78  bibsource = {dblp computer science bibliography, http://dblp.org}
     79}
     80
     81@phdthesis{bac-thesis08,
     82  title = {Type-based amortized stack memory prediction},
     83  author = {Brian Campbell},
     84  school = {University of Edinburgh},
     85  year = 2008
     86}
     87
     88@inproceedings{bac-giveback08,
     89  title = {Prediction of linear memory usage for first-order functional programs},
     90  author = {Brian Campbell},
     91  booktitle = {Trends in Functional Programming},
     92  editor = {Peter Achten and Pieter Koopman and Moraz\'an, Marco T.},
     93  volume = 9,
     94  year = 2009,
     95  pages = {1--16},
     96  publisher = {Intellect},
     97  isbn = {978-1-84150-277-9}
     98}
     99
     100@inproceedings{bac-esop09,
     101  title = {Amortised Memory Analysis using the Depth of Data Structures},
     102  author = {Brian Campbell},
     103  booktitle = {Programming Languages and Systems: 18th European Symposium on Programming (ESOP 2009)},
     104  pages = {190--204},
     105  year = 2009,
     106  editor = {Giuseppe Castagna},
     107  volume = 5502,
     108  series = {Lecture Notes in Computer Science},
     109  publisher = {Springer-Verlag},
     110  doi = {10.1007/978-3-642-00590-9_14}
     111}
     112
     113@article{ASPINALL2007411,
     114title = "A program logic for resources",
     115journal = "Theoretical Computer Science",
     116volume = "389",
     117number = "3",
     118pages = "411 - 445",
     119year = "2007",
     120note = "",
     121issn = "0304-3975",
     122doi = "http://dx.doi.org/10.1016/j.tcs.2007.09.003",
     123url = "http://www.sciencedirect.com/science/article/pii/S0304397507006627",
     124author = "David Aspinall and Lennart Beringer and Martin Hofmann and Hans-Wolfgang Loidl and Alberto Momigliano",
     125}
     126
     127@inproceedings{DBLP:conf/esop/HofmannJ06,
     128  author    = {Martin Hofmann and
     129               Steffen Jost},
     130  title     = {Type-Based Amortised Heap-Space Analysis},
     131  booktitle = {Programming Languages and Systems, 15th European Symposium on Programming,
     132               {ESOP} 2006, Held as Part of the Joint European Conferences on Theory
     133               and Practice of Software, {ETAPS} 2006, Vienna, Austria, March 27-28,
     134               2006, Proceedings},
     135  pages     = {22--37},
     136  year      = {2006},
     137  crossref  = {DBLP:conf/esop/2006},
     138  url       = {http://dx.doi.org/10.1007/11693024_3},
     139  doi       = {10.1007/11693024_3},
     140  timestamp = {Thu, 28 May 2015 17:23:23 +0200},
     141  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/esop/HofmannJ06},
     142  bibsource = {dblp computer science bibliography, http://dblp.org}
     143}
     144
     145@inproceedings{HoffHof10,
     146  author    = {Jan Hoffmann and
     147               Martin Hofmann},
     148  title     = {{Amortized Resource Analysis with Polynomial Potential - A
     149             Static Inference of Polynomial Bounds for Functional Programs}},
     150  booktitle = {{In Proceedings of the 19th European Symposium on Programming (ESOP'10)}},
     151  pages     = {287-306},
     152  publisher = {Springer},
     153  series    = {Lecture Notes in Computer Science},
     154  volume    = {6012},
     155  year      = {2010}
     156}
     157
     158
     159@article{HAH12Toplas,
     160 author = {Jan Hoffmann and Klaus Aehlig and Martin Hofmann},
     161 title = {{Multivariate Amortized Resource Analysis}},
     162 journal = {ACM Trans. Program. Lang. Syst.},
     163 issue_date = {October 2012},
     164 volume = {34},
     165 number = {3},
     166 month = nov,
     167 year = {2012},
     168 issn = {0164-0925},
     169 pages = {14:1--14:62},
     170 articleno = {14},
     171 numpages = {62},
     172 url = {http://doi.acm.org/10.1145/2362389.2362393},
     173 doi = {10.1145/2362389.2362393},
     174 acmid = {2362393},
     175 publisher = {ACM},
     176 address = {New York, NY, USA},
     177 keywords = {Amortized analysis, functional programming, quantitative analysis, resource consumption, static analysis},
    52178}
    53 
    54179
    55180
  • Papers/jar-cerco-2017/conclusions.tex

    r3647 r3648  
    6767As a result, one could potentially imagine pairing the loop-bound analysis with our parametric cost model to reduce the amount of user interaction required when using it.
    6868
    69 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.
     69Abstract 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.
     70
     71\paragraph{Type- and program logic-based analyses}
     72
     73Resource Aware ML (RAML) is a first-order statically typed functional programming language~\cite{Hoffmann11,HAH12Toplas,HoffHof10}.
     74The RAML type system is able to derive polynomial resource bounds from first-order functional programs, using a variant of the `potential method'.
     75This 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.
     76Campbell also used a variant of this approach to predict stack space usage~\cite{bac-thesis08,bac-giveback08,bac-esop09}.
     77
     78% implicit computational complexity
     79
     80Several program logics for reasoning about a program's resource consumption have been investigated in the literature.
     81
     82Aspinall 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}.
     83The soundness of the logic was formally verified in Isabelle/HOL.
     84Along 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}.
     85The soundness of the logic was also formally verified, using the Coq proof assistant.
     86This work will be further discussed below.
    7087
    7188\subsubsection{High-level approaches}
     
    8198Nevertheless, despite these differences, the two projects are clearly closely related.
    8299
    83 \paragraph{Type-based analyses}
     100\paragraph{Verified compilation}
    84101
    85 Resource Aware ML (RAML) developed by Hoffmann and Hoffmann is a first-order statically typed functional programming language.%cite
    86 RAML's sophisticated type system is able to
     102% CompCert, CompCertTSO, CakeML, C0, etc.
    87103
    88104\subsection{Further work}
Note: See TracChangeset for help on using the changeset viewer.