This paper outlines the structure of a formalism intended to aid in the
design and analysis of linking systems. Cardelli begins by providing a
motivation for the study of this topic by illustrating several of the pitfalls
faced in the development of software consisting, in the typical fashion, of
multiple interacting modules. To provide a concrete source language that
supports modules an extension to the simply-typed lambda calculus is proposed.
While this extension is syntactically informal (the syntax of F1 is not
extended; rather sample notation that characterizes the nature of the extension
is given), the type system and judgements in that system are extended to
support the semantics of the module extension - these are termed bindings and
signatures.
The notion of a linkset is expressed partly in terms of the vocabulary used
in the module extension to F1. Intuitively, a linkset is a sequence of type
judgements, each based on an internal and external typing environment. The
external typing environment corresponds to definitions of free-variables in the
program, imported say from an external library, while the internal environment
constitutes the immediate compilation environment of the program fragment that
is being judged. The operations permissible on a linkset include evaluating the
type-consistency of each of the judgements as well as performing substitutions
of terms in accordance with the type judgements. This second operation
(substitution) is formalised as the process of linking and an algorithm that
performs this operation presented.
The paper concludes with a discussion of the relationship between the
modules of the F1 extension and the linkset formalism. A procedure to convert
the signature-bindings to linksets is presented - it is this process that is
referred to as "compilation". It is proved that this operation preserves the
type-consistency of the module/linkset. Hence separate compilation is reliable.
This paper is useful in that it extends the familiar machinery of a type
system to express the problem of linking. It is, however, only a beginning, and
as much is admitted by the author. The most striking simplifying assumption is
the non-existence of circular dependencies including recursion.
This paper aims to show how a linker can work "correctly" in a simplified environment. The author starts by describing many problems that are faced during a modern software development scenario. After this background, the author punts many of the problems in the current software cycle to focus on a simplified formalism of linking. In the beginning sections, the author spends considerable time developing a simple typed lambda calculus (F1) that's used for the proofs later in the paper. The idea of linksets are developed and then the author shows how linking can be viewed as "the repeated application of type-preserving substitutions". A similar approach is taken for describing modules. The basic idea is to view a module as a linkset and then most of the rules from before seem to fall into place. The author finishes up by providing some proofs to show that compilation occurs as expected.
The problem this paper approaches is finding a way to ensure that pre-compiled modules that are linked to create a program can indeed be linked, and there are no versioning or interface problems that will cause the resulting program to malfunction. The author begins by describing the problem, and giving examples of cases that even if linking succeeds, the resulting program might not be correct. The solution he proposes is a formal way of describing the "interfaces" between modules using types in a typed lambda-calculus language (F1). That is not the same as the usual module interfaces on which current linking is based. A formal way of stating the types that a module "imports" or "exports" is presented. The concept of linkset as the type-interface of a module is defined, and a framework of manipulating linksets is presented. Finally, the author uses that framework to present a linking algorithm which is proven to be sound, and, if successful, to create a program without problems resulting from incorrect linking between incompatible modules. In detail, first, the step of linking two modules is defined. That corresponds to the combination of two linksets, to produce a third linkset. Each linkset has a set of "imported" and a set of "exported" types. During linking of two modules, some imports are satisfied. The algorithm iterates applying that step, resulting in a final linkset without imports (the closure on the link operation - which is the final program), or reports failure, if there is no way to proceed and not all imports are satisfied. That algorithm introduces another check that can be done during linking, that enforces more restrictions than actual object code-linking was using until now/ Therefore, it can "catch" more erroneous cases.
In this paper, the notion that linking should be treated more than just a formality of gluing together code, but as a necessary and important step of compilation. This is concretized by treating program fragments as portions of a linkset, where each fragment is represented as type judgment. Furthermore, each judgment is represented as a module, with imports defined as the judgement's assumed environment (lhs), and exports defined as the outermost expressions of the judgment (rhs). In typical compilation systems, a set of modules links if and only if, along with some predefined external dependencies, all dependencies between modules are satisfied. In the Cardelli system, a linkset is valid if and only if, along with some base environment, all module environments can be reduced to null. This has the nice property that linking can thus be reduced to typechecking. Although this system is nice for the simply typed lambda calculus, it does not cover several key requirements of more real-world applications (although these shortcomings are acknowledged by the author). It does not handle recursive dependencies, either inter-modular or intra-modular (recursive lambda abstractions). Subtyping is not handled either, although there is brief mention of it in Def. 5.4.
Luca Cardelli proposes a formal description of linking for a simple typed-lambda language. In his framework, a program fragment is a set of lambda-expressions which may have free variables, and a complete program is a closed lambda-expression. Each fragment is labeled, and each label is a set of names which can be free variables in other fragments. In terms of a C-like language, a program fragment is a set of functions or global variables, and the label is the corresponding set of names assigned. All the free variables are assigned types before the linking process can begin. The actual process of linking is straightforward: each fragment has an environment listing its free variable (imports), and a label listing the variables it provides (exports). The linker checks that a variable needed by one fragment matches the type of the appropriately named variable provided by another fragment. Cardelli doesn't address circular dependencies, so once it's determined that the types are compatible, the linker does variable substitution and arrives at a slightly smaller link set. Eventually the fragments all get merged into either a complete program, or a more complete fragment. The paper works under the assumption that type-checking the fragments is the hardest part of linking. This makes sense in the simple language used, but it's not clear how well the concepts in the paper could be applied to a current language. Still for the language described, the framework can do a lot. For example, if the modules keep their labels after substitution, then the framework could support 'unlinking' modules and we could, for example, change a small portion of a library and re-link it without having to re-link the entire library.
Cardelli presents a compelling case for the study of linking systems at the beginning of the paper. Despite some bizarre English at times, e.g. "This happens for generic module mechanism in the style on templates", the paper is fairly readable, as papers about formalisms go. As this was one of the first papers studying linkers formally, the primary contribution is establishing a way of talking about linking, and defining some basic soundness properties within this system. The ideas are not new, it is simply a matter of describing them precisely. The paper provides good motivation for the study of linkers, and leaves us with a foundation for further papers with more to say.
This paper introduces introduces a framework around a simple language for type checking independently developed program modules. Typechecked modules are essentially left with a signature that can be used for checking compatibility against other modules. The notion of a linkset is introduced, a group of program fragments which contains an import environment (dependencies) and an export environment (things which may be linked to from other modules). In the paper only the type checking aspects of programming are considered, as modules are essentially compiled into these linksets. Rules are given for compatibility checking as well as for merging and reduction of compatible linksets. As motivation the paper lists several current pitfalls(circa 1996, though no doubt still true today) with type checking in the presense of dynamic and static linking mostly focussing on book-keeping as modules are updated. The body of the paper though appears to mostly ignore this list of problems as it develops its notation and rules for linksets.
This paper is primarily concerned with formalizing linking and modularization in the context of separate compilation. The notion of modules and interfaces discussed in this paper is more along the ?classic? interpretation involving separate compilation and not of any sort of language construct. The author starts out by sketching a generic scenario involving separate compilation and linking (with semantics similar to Java) and then pointing out many problems areas for each step of the scenario. At this point, the reader is convinced that modularization and linking are quite complex in today?s world and, at the very least, demand careful thought. In simple terms, linking can be thought of as a series of substitutions. To demonstrate this statement, the author introduces formalism. This formalism defines the notions of program fragments, environments, linksets, and introduces a language F1 based on lambda calculus. After repeated substitution, once the environments of all program fragments are empty, the program is complete. I believe the author has succeeded in jump starting formal thinking of separate compilation and linking.
Sorry for Late Submission Review: In this paper, author provided a formal interpretation for linking and separate compilation by formalizing linking via linkset and separation compilation as the ability to translate modules to linkset that can be linked safely. Also in this framework, author proved that separately compiled, compatible modules could be linked together safely using formal language. Firstly, by introducing an example of software development cycle, author stated the importance of linking and separate compilation and motivation of developing a formalized process to check the accuracy. Then he constructed a simple typed lambda calculus (F1) environment to adapt his idea by making many simplification and assumption. After that, the key part of this paper discussed the Linkset that comes from separately compiled module and the properties for linking step. In the end, this paper outlined an inference system to establish the soundness of sequence of compilation and linking steps. I think this paper is fun, turn a big problem to a restricted problem that can be formalized. The basic ideas here are useful when we want to make sure and analysis the correctness of the linking step in our system. Also the direction for the further researching is interesting and worth thinking.
The paper by Luca Cardelli gives a good insight of Linking and concept of the seperate compilation.This paper considers linking as the fundamental process from which midule mechanism arise.In the begning of the paper there explanation of Lambada Calculus on which the proofs are based in the later part of the paper.Linking is defined as the process which truns the a collection of the program fragments into executable form.Its also explains the some of the terms like Complete Program(Program which has no free terms),Library(Results from the incomplete linking). The concept of linkset through which the linking is formalised is well explained in the paper.Linksets are the collection of the linkable fragments.Program fragments have interfaces in terms of "Import Type" and "Export Type".The main activities perofrmed on the linksets are:Name Checking and Type Checking.The terms Intera Module Type Checking and Inter Module Type checking are well defined in the paper. Linkset Merge is carried out to combine the multiple modules into linkable form ie merging of two or more linksets.Many methods of manuplating linksets are explained in the paper .According to the paper if two modules are seperately typed checked and have Compatible interfaces then their complied fragments can be merged and linked.Concept and importance of the inteface is well defined in the paper.
The paper by Luca Cardelli gives a good insight of Linking and concept of the seperate compilation.This paper considers linking as the fundamental process from which midule mechanism arise.In the begning of the paper there explanation of Lambada Calculus on which the proofs are based in the later part of the paper.Linking is defined as the process which truns the a collection of the program fragments into executable form.Its also explains the some of the terms like Complete Program(Program which has no free terms),Library(Results from the incomplete linking). The concept of linkset through which the linking is formalised is well explained in the paper.Linksets are the collection of the linkable fragments.Program fragments have interfaces in terms of "Import Type" and "Export Type".The main activities perofrmed on the linksets are:Name Checking and Type Checking.The terms Intera Module Type Checking and Inter Module Type checking are well defined in the paper. Linkset Merge is carried out to combine the multiple modules into linkable form ie merging of two or more linksets.Many methods of manuplating linksets are explained in the paper .According to the paper if two modules are seperately typed checked and have Compatible interfaces then their complied fragments can be merged and linked.Concept and importance of the inteface is well defined in the paper.
The paper is trying to state the importance of separate compilation and linking
process Which should be used in the now a day’s modular approach to
programming. The very basic aim of modularization in programming is to make the
different modules reusable and with different modules. This very purpose cannot
be achieved if the different modules, which change into object code on
compilation, are not compatible with each other during linking. The paper
devotes time in defining terms like Linkset and laying down rules for
successful linking of two linksets. The paper says that modularization and the
concept of separate compilation and linking go together and cannot be
separated.
A linkset is defined as a collection of fragments that can be linked. This
mayor may not generate a final executable program as it may turn out to be a
library. These libraries may further be linked to form new libraries or
executable programs.
Now the rules for successful linking of different modules after
compiling.
According to the paper the two main functions that we can perform on linksets
is checking their name and type. The name checking ensures inter and intra
modular type checking. So the properties of a good linkset can be said as Type
Checked,Inter Checked and no clashes of names. The paper has come very close to
define linking as mere substitution.
I feel that the paper was successful n formalizing linking. The paper
does not Say anything about dynamic linking which I think is a very important
topic in this context and should have been addressed.
I'm not officially in the class, but I thought I'd do a review as well. I generally associate Cardelli with another type theory guy, Abadi. Both use type theory to characterize real programs. Basically, Cardelli is saying that separate compilation and linking is something that PL folks need to sit down and formalize. He claims that without such formalizations, certain properties are difficult to prove and to reason about. Of course, *anyone* can say "we need to formalize linking". To get a paper out of this, you need to have some scheme for demonstrating what linking means, and preferably, show that such a scheme is simple enough to be understood, realistic enough so that it captures some features of real linking. To this end, his goal is not to look at linking mechanisms for languages such as C, but to approach the problem from what he's good at: type theory/lambda calculus. There's a question as to whether this approach is a reasonable one. How well does it model "real" languages. The advantage of using lambda calculus is twofold. First, lambda calculus been around a while. Certainly, the functional programming language community is very familiar with lambda calculus. People know how to prove properties about the lambda calculus, so there's a CS audience who will agree that it's reasonable. Second, there are real languages based on this formalism (ML, Haskell, etc). So, there's no need to convince CS types that this formalism doesn't apply to "real" languages. The paper is mostly proof-of-concept. Cardelli's intention doesn't seem to be solving the problem of linking in a completely realistic manner. Indeed, he cites many ways his work can be extended to capture a more realistic system. Instead, he merely shows that, with a fairly simple, formal model, he can capture the important features of linking, reason about various properties, and then leave it open to others (possibly including himself) to do the nastier extensions to the ideas. This isn't to say the paper isn't important, because, presumably, prior to his paper, people hadn't thought about expressing linking in a formal way, or at least, perhaps no one of Cardelli's caliber. It's not necessary for Cardelli to handle formalization. Sometimes it's merely enough for him to tell the PL community that this is something they need to consider. If his point is to say "nice properties can be shown in a simple, formal framework", then that's something PL researchers, and even PL practioners, can embrace.
Generated: Thu Mar 6 15:39:24 EST 2003 by mwh