Show simple item record

dc.contributor.author
Kogtenkov, Alexander
dc.contributor.supervisor
Meyer, Bertrand
dc.contributor.supervisor
Furia, Carlo A.
dc.contributor.supervisor
Mazzara, Manuel
dc.contributor.supervisor
Meijer, Erik
dc.contributor.supervisor
Thiele, Lothar
dc.date.accessioned
2017-05-30T14:00:36Z
dc.date.available
2017-05-23T15:42:32Z
dc.date.available
2017-05-25T21:09:25Z
dc.date.available
2017-05-26T08:27:06Z
dc.date.available
2017-05-30T08:35:58Z
dc.date.available
2017-05-30T14:00:36Z
dc.date.issued
2017-01-31
dc.identifier.uri
http://hdl.handle.net/20.500.11850/135
dc.identifier.doi
10.3929/ethz-b-000000135
dc.description.abstract
Null pointer dereferencing is a well-known issue in object-oriented programming, and can be avoided by adding special validity rules to the programming language. However, just introducing a single rule is not enough: the whole language infrastructure has to be considered instead. The resulting guarantees are called void safety. The thesis reviews, in detail, engineering solutions and migration efforts that enabled the transition from classic to void safe code of multiple libraries and projects with lines of code ranging in the millions. Experience with the tiny details of the implementation can be an invaluable source of insight for researcher looking into making a language void safe. The void safety rules can be divided into three major categories. The first one is the extension of a regular type system with attached (non-null) and detachable (possibly-null) types. Generic programming opens a door to different interpretations. The thesis defines some base void safety properties for formal generic types and specifies void-safety-aware conformance rules. The second category of rules ensures that newly created objects reach a stable state maintaining the type system guarantees. The thesis proposes two solutions for this object initialization issue and compares them to previous work. It formalizes the rules in the Isabelle/HOL proof assistant and establishes some of their properties. To ensure safety at the end of object life cycle it also specifies validity rules for finalizers. A number of examples are used to demonstrate that the proposed solutions are of practical use and do not suffer from limited expressiveness caused by the lack of additional annotations describing intermediate object states. The third category of void safety rules covers a practical need to bridge the gap between attached and detachable types. The thesis proposes formal void safety rules for local variables in the context of an object-oriented language that do not require any marks to distinguish between attached and detachable types. It demonstrates advantages of the annotation-free approach with benchmarks based on open source code, discusses implementation decisions and how they are reflected in the formal model. The thesis concludes with a machine-checkable soundness proof for the rules involving local variables using the Isabelle/HOL proof assistant.
en_US
dc.format
Adobe PDF
en_US
dc.language.iso
en
en_US
dc.publisher
ETH Zurich
en_US
dc.rights.uri
http://creativecommons.org/licenses/by-nc-sa/4.0/
dc.subject
void safety
en_US
dc.subject
null safety
en_US
dc.subject
static analysis
en_US
dc.subject
object initialization
en_US
dc.subject
operational semantics equivalence
en_US
dc.subject
Eiffel
en_US
dc.subject
certified attachment pattern
en_US
dc.subject
object-oriented language safety
en_US
dc.subject
source code safety benchmark
en_US
dc.subject
big-step operational semantics
en_US
dc.subject
formal methods
en_US
dc.subject
software modularity
en_US
dc.subject
null reference
en_US
dc.subject
null pointer dereferencing
en_US
dc.title
Void safety
en_US
dc.title.alternative
Avoiding Null Pointer Dereferencing in an Object-Oriented Language
en_US
dc.type
Doctoral Thesis
dc.rights.license
Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International
dc.date.published
2017-05-25
ethz.size
321 p.
en_US
ethz.code.ddc
DDC - DDC::0 - Computer science, information & general works::004 - Data processing, computer science
en_US
ethz.identifier.diss
24129
en_US
ethz.publication.place
Zurich
en_US
ethz.publication.status
published
en_US
ethz.leitzahl
02150 - Departement Informatik / Department of Computer Science::03594 - Meyer, Bertrand (emeritus)
en_US
ethz.leitzahl.certified
02150 - Departement Informatik / Department of Computer Science::03594 - Meyer, Bertrand (emeritus)
en_US
ethz.relation.cites
10.1007/978-1-84882-912-1_9
ethz.relation.cites
10.15514/ISPRAS-2016-28(5)-2
ethz.relation.cites
http://drdobbs.com/architecture-and-design/219500827
ethz.relation.cites
10.1016/j.scico.2013.11.006
ethz.relation.cites
http://arxiv.org/abs/1307.3189
ethz.date.deposited
2017-05-23T15:42:32Z
ethz.source
FORM
ethz.eth
yes
en_US
ethz.availability
Open access
en_US
ethz.rosetta.installDate
2017-06-02T00:00:00Z
ethz.rosetta.lastUpdated
2020-02-14T04:00:49Z
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=Void%20safety&rft.date=2017-01-31&rft.au=Kogtenkov,%20Alexander&rft.genre=unknown&rft.btitle=Void%20safety
 Search print copy at ETH Library

Files in this item

Thumbnail

Publication type

Show simple item record