Flexible Dynamic Linking
Thesis
Portability of programs between run-time environments is regarded as a desirable feature by programmers and users. In a modern virtual machine like the JVM, portability is supported by large standard libraries. A program that uses an interface from a standard library should be portable to any run-time environment that provides an implementation of the interface. Because different implementations of an interface have different names, a programmer who desires portability must write code to select an implementation. This introduces software engineering costs and type-safety concerns.
We believe that dynamic linking is well-suited to providing portability automatically. Linking traditionally requires that types from the compile-time environment are present in the run-time environment. We suggest "flexible" dynamic linking that relaxes a program's dependencies on compile-time types in a type-safe and language-independent way, thus providing portability to different run-time environments. Bytecode is annotated with type variables rather than type names, and a non-deterministic model substitutes type variables with type names during linking. We interleave linking with execution, as in the JVM, and examine how linking builds a well-formed program. We prove soundness for any substitution strategy, representing execution with an arbitrary degree of eagerness/laziness in linking.
We then explore portability in the Common Language Infrastructure (CLI). We formalise its component, linking and execution models to show the flexibility of existing link-time mechanisms, and how linking varies between CLI implementations like .NET, Mono and Rotor. The CLI's reflection mechanism is often used by programmers to facilitate portability, but reflection introduces many complexities into linking and execution that we formalise accurately. Then, as an alternative to reflection, we design flexible dynamic linking for the CLI and implement it in the Rotor virtual machine. In this scheme, a programmer controls portability by identifying potential substitutions explicitly, thus losing the generality of reflection but ensuring predictability and type-safety.
Thesis (PDF), February
2007
Supervisors: Sophia Drossopoulou and Susan Eisenbach
Examiners:
David Rosenblum
and Peter Henderson
Papers
- Flexible Dynamic Linking for .NET
- with Anders Aaltonen and Susan Eisenbach
- at the 4th International Conference on .NET Technologies, Plzen, Czech Republic, May 2006
- A Model of Dynamic Binding in .NET
- At the 3rd International Working Conference on Component Deployment, Grenoble, November 2005
- And
- At the 7th ECOOP Workshop on Formal Techniques for Java-like Programs, Glasgow, Scotland, July 2005
- And
- Flexible Bytecode for Linking in .NET
- with Michelle Murray, Susan Eisenbach and Sophia Drossopoulou
- at the 1st ETAPS Workshop on Bytecode Semantics, Verification, Analysis and Transformation, Edinburgh, Scotland, April 2005
- Safety in Flexible Dynamic Linking
- with Sophia Drossopoulou
- October 2004
- Flexible Dynamic Linking
- with Sophia Drossopoulou
- at the 6th ECOOP Workshop on Formal Techniques for Java-like Programs, Oslo, Norway, June 2004
Projects
- Susan Eisenbach and I received a grant for "Safe and Flexible Dynamic Linking for .NET" from Microsoft Research under the SSCLI RFP II program in 2004. (Final presentation in Seattle, September 2005.)
- I have co-supervised four individual projects and one group project on implementing flexible dynamic linking for the JVM and .NET.
- D.Wong (Comp MEng4 individual project)
- A.Aaltonen (JMC MEng4 individual project)
- M.Uttamchandani (Comp MEng4 individual project)
- M.Murray (MSc Conversion individual project)
- A.Mohri, M.Puzovic et al (JMC BEng3 group project)
- A.Aaltonen (JMC MEng4 individual project)
- I have supervised one individual and one group project on other topics.
- M.Breza, M.Kay et al (MSc Conversion group project) - "whoknows 2005"
- L.Guillemaille (Comp MEng4 individual project) - "MemosByMail"
Conference and workshop attendance
- .NET Technologies 2006
- Plzen, Czech Republic, May 2006
- Microsoft SSCLI RFP II Capstone
- Seattle, Washington, USA, September 2005
- ECOOP 2005, inc. FTfJP (Workshop on Formal Techniques for Java-like Programs)
- Glasgow, Scotland, July 2005
- BYTECODE 2005 (Workshop on Bytecode Semantics, Verification, Analysis and Transformation) at ETAPS 2005
- Edinburgh, Scotland, April 2005
- POPL 2005, inc. TLDI'05 (2nd ACM SIGPLAN Workshop on Types in Language Design and Implementation), FOOL 12 (12th International Workshop on Foundations of Object-Oriented Languages) and PLAN-X 2005 (Programming Language Technologies for XML)
- Long Beach, California, USA, January 2005
- WOOD 2004 (2nd Workshop on Object-Oriented Developments) and FGUC 2004 (Joint 3rd Workshop on Foundations of Global Ubiquitous Computing) at CONCUR 2004
- London, UK, September 2004
- ECOOP 2004, inc. PPPL (Practical Problems of Programming in the Large Workshop) and FTfJP (Workshop on Formal Techniques for Java-like Programs)
- Oslo, Norway, June 2004
Miscellaneous activities
- I have reviewed papers for numerous international conferences and
workshops on programming languages and software engineering, including
ECOOP, CBSE, Journal of Object Technology, Formal Techniques for
Java-like Programs, and .NET Technologies.
- I am a member of the SLURP reading group that discusses new papers on object-oriented topics.
- I read the TYPES and New Jersey Programming Languages Seminar (NJPLS) mailing lists.
- SCHOOL: a Small Chorded Object-Oriented Language
- I am a member of the SLURP reading group that discusses new papers on object-oriented topics.
- with Sophia Drossopoulou, Alexis Petrounias and Susan Eisenbach
- March 2005