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.
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.