CMSC 838Y Paper Reviews

Skip down to paper 0: Luca Cardelli. Program Fragments, Linking, and Modularization. In SIGPLAN Symposium on the Principles of Programming Languages, pages 266-277. ACM, January 1997. [ .ps ]


Reviews for paper 0

Review from Nikhil Swamy <nswamy@cs> at Wed Feb 5 14:10:36 EST 2003:

    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. 

Review from Bryan Payne <bdpayne@cs> at Wed Feb 5 22:02:46 EST 2003:

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.

Review from Polyvios Pratikakis <polyvios@cs.umd.edu> at Thu Feb 6 10:49:39 EST 2003:

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.

Review from Jeff Odom <jodom@cs.umd.edu> at Thu Feb 6 11:30:26 EST 2003:

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.

Review from Nate Waisbrot <waisbrot@cs> at Thu Feb 6 11:44:17 EST 2003:

	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.

Review from James Rose <rosejr@cs> at Thu Feb 6 12:06:10 EST 2003:

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.

Review from Brian K at Thu Feb 6 12:25:10 EST 2003:

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. 

Review from Mujtaba Ali <mujtaba@bitsmart.com> at Thu Feb 6 12:27:04 EST 2003:

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.

Review from yuanyuan@cs at Thu Feb 6 16:52:19 EST 2003:


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.



Review from plamba@wam.umd.edu at Thu Feb 6 18:03:06 EST 2003:

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.


Review from plamba@wam.umd.edu at Thu Feb 6 18:03:35 EST 2003:

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.


Review from piyush bhagat <piyushb@glue.umd.edu> at Thu Feb 6 20:02:21 EST 2003:


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.    

Review from Charles Lin at Fri Feb 14 09:45:24 EST 2003:

   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


mwh@cs.umd.edu

Web Accessibility