research-article

Static techniques for reducing memory usage in the C implementation of whiley programs

Authors:

Min-Hsien Weng,

Bernhard Pfahringer,

Mark UttingAuthors Info & Claims

ACSW '17: Proceedings of the Australasian Computer Science Week Multiconference

Article No.: 15, Pages 1 - 8

https://doi.org/10.1145/3014812.3014827

Published: 31 January 2017 Publication History

Get Access

Abstract

Languages that use call-by-value semantics, such as Whiley, can make program verification easier. But efficient implementation becomes harder, due to the overhead of copying and garbage collection. This paper describes how a mixture of static analysis and runtime-monitoring can be used to eliminate unnecessary copying and deallocate memory without garbage collection. We show that this allows Whiley programs to be translated into efficient C implementations.

References

[1]

A. V. Aho, R. Sethi, and J. D. Ullman. Compilers, Principles, Techniques, chapter 9, page 608. Addison wesley, 2006.

Digital Library

Google Scholar

[2]

J. Aldrich, V. Kostadinov, and C. Chambers. Alias Annotations for Program Understanding. In ACM SIGPLAN Notices, volume 37, pages 311--330. ACM, 2002.

Digital Library

Google Scholar

[3]

A. Alexandrescu. Modern C++ design: generic programming and design patterns applied. Addison-Wesley, 2001.

Digital Library

Google Scholar

[4]

J. Blandy. Why Rust? Trustworthy, Concurrent Systems Programming. Number 978-1-491-92730-4. O'Reilly Media, Inc., First edition, September 2015.

Google Scholar

[5]

N. Lameed and L. Hendren. Staged static techniques to efficiently implement array copy semantics in a MATLAB JIT compiler. In Compiler Construction, pages 22--41. Springer, 2011.

Digital Library

Google Scholar

[6]

N. Nethercote and J. Seward. Valgrind: a framework for heavyweight dynamic binary instrumentation. In ACM Sigplan notices, volume 42, pages 89--100. ACM, 2007.

Digital Library

Google Scholar

[7]

D. J. Pearce. Integer range analysis for Whiley on embedded systems. In Object/Component/Service-Oriented Real-Time Distributed Computing Workshops (ISORCW), 2015 IEEE International Symposium on, pages 26--33. IEEE, 2015.

Digital Library

Google Scholar

[8]

D. J. Pearce and L. Groves. Designing a verifying compiler: Lessons learned from developing Whiley. Science of Computer Programming, 113:191--220, 2015.

Digital Library

Google Scholar

[9]

P. Schnorf, M. Ganapathi, and J. L. Hennessy. Compile-time Copy Elimination. Software: Practice and Experience, 23(11):1175--1200, 1993.

Digital Library

Google Scholar

[10]

M.-H. Weng, M. Utting, and B. Pfahringer. Bound Analysis for Whiley Programs. Electronic Notes in Theoretical Computer Science, 320:53--67, 2016.

Digital Library

Google Scholar

Cited By

View all

Weng MMalik RUtting M(2021)Automatic proofs of memory deallocation for a Whiley-to-C CompilerFormal Methods in System Design10.1007/s10703-021-00378-0Online publication date: 16-Aug-2021
https://doi.org/10.1007/s10703-021-00378-0
Pearce DUtting MGroves L(2019)An Introduction to Software Verification with WhileyEngineering Trustworthy Software Systems10.1007/978-3-030-17601-3_1(1-37)Online publication date: 14-Apr-2019
https://doi.org/10.1007/978-3-030-17601-3_1

Index Terms

Static techniques for reducing memory usage in the C implementation of whiley programs
1. Software and its engineering
  1. Software organization and properties
    1. Extra-functional properties
      1. Software performance
    2. Software functional properties
      1. Correctness
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis

Recommendations

Bound Analysis for Whiley Programs

The Whiley compiler can generate naive C code, but the code is inefficient because it uses infinite integers and dynamic array sizes. Our project goal is to build up a compiler that can translate Whiley programs into efficient OpenCL code with fixed-...
A comparative study of static CIA techniques
Internetware '12: Proceedings of the Fourth Asia-Pacific Symposium on Internetware

Software Change Impact Analysis (CIA) is an essential technique to identify the unpredicted and potential effects caused by software changes. A rich body of different CIA techniques, especially static CIA techniques, have continuously emerged in recent ...
Machine-learning-guided selectively unsound static analysis
ICSE '17: Proceedings of the 39th International Conference on Software Engineering

We present a machine-learning-based technique for selectively applying unsoundness in static analysis. Existing bug-finding static analyzers are unsound in order to be precise and scalable in practice. However, they are uniformly unsound and hence at ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACSW '17: Proceedings of the Australasian Computer Science Week Multiconference

January 2017

615 pages

ISBN:9781450347686

DOI:10.1145/3014812

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 31 January 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ACSW 2017

ACSW 2017: Australasian Computer Science Week 2017

January 30 - February 3, 2017

Geelong, Australia

Acceptance Rates

ACSW '17 Paper Acceptance Rate 78 of 156 submissions, 50%;

Overall Acceptance Rate 204 of 424 submissions, 48%

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
60
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 19 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Weng MMalik RUtting M(2021)Automatic proofs of memory deallocation for a Whiley-to-C CompilerFormal Methods in System Design10.1007/s10703-021-00378-0Online publication date: 16-Aug-2021
https://doi.org/10.1007/s10703-021-00378-0
Pearce DUtting MGroves L(2019)An Introduction to Software Verification with WhileyEngineering Trustworthy Software Systems10.1007/978-3-030-17601-3_1(1-37)Online publication date: 14-Apr-2019
https://doi.org/10.1007/978-3-030-17601-3_1

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Bound Analysis for Whiley Programs

A comparative study of static CIA techniques

Machine-learning-guided selectively unsound static analysis