This new version of the conductor software forms the infrastructure
of the ConCert grid. The software is responsible for distributing
and running the certified computations (called "cords") and for
interfacing with application software.
The ConCert software implements the scheduling, distribution,
and verification of computation on the grid. This software
is required to participate on the ConCert grid framework.
More documentation about the ConCert software and framework
can be found in DeLap's senior thesis
[DeL02]. This version is obsoleted
by the above.
The ConCert Simulator provides a SML library that implements
as closely as possible the proposed high-level programming
language for programming in ConCert. It does not run tasks
on the grid but rather simulates ConCert tasks running on
the grid by threads running on the local system. The
proposed high-level programming interface cannot be
implemented directly in SML, so certain compromises had to
be made; however,these were kept to a minimum. More
documentation about the proposed high-level programming
interface and the simulator can be found in Chang's senior thesis
[Cha02].
Requires
Standard ML of New Jersey
(SML/NJ)
110 compiler with
Concurrent ML
(CML)
Versions
0.1
(05/15/2002) - The first pre-release version.
CML is used to simulate on the local system ConCert tasks
running on the grid.
Iktara is a linear logic theorem prover intended to run on
the ConCert grid framework. The development of Iktara
has served to guide the design of a high-level programming
interface for programming in ConCert. More documentation
about the theorem proving algorithm and the adaptation for
the ConCert framework can be found in Chang's senior thesis
[Cha02].
Requires
Standard ML of New Jersey
(SML/NJ)
110 compiler with
Concurrent ML
(CML)
0.1
(05/15/2002) - The first pre-release version. There are
three versions of Iktara: a sequential implementation
in SML without any extensions, a concurrent implementation
in CML, and an implementation that runs on the ConCert
simulator.