|
|
occam-pi: blending the best of CSP and the pi-calculus |
[ news | occam-pi | download | documentation | bugs | coming-soon | publications | links ]
Occam-pi and KRoC are the result of on-going research extending the (CSP) ideas of occam by judicious inclusion of the mobility features of the pi-calculus. In the interests of proveability, we have been careful to preserve the distinction between the original simple static point-to-point synchronised communication of occam and the dynamic asynchronous multiplexed communication of the pi-calculus; in this we have been prepared to sacrifice the elegant sparsity of the pi-calculus. We conjecture that the extra complexity (and discipline) introduced will make the task of proving concurrent and distributed programs easier.
The Kent Retargetable occam Compiler (KRoC) is an occam/occam-pi language platform, comprised of an occam compiler, native-code translator and supporting run-time system.
This page documents the open-source (GNU General Public License (GPL) and Library General Public License (LGPL)) version of KRoC, currently supporting Intel/i386 based machines running Linux or FreeBSD. Binary releases of older versions of KRoC (that do not support the occam-pi extensions) are available for Solaris/SPARC, OSF/Alpha and Parsytec/PowerPC, from the WoTUG site.
CSP has a compositional and denotational semantics, which means that it allows modular and incremental development (refinement) even for concurrent components. In turn, this means that we get no surprises when we run processes in parallel (since their points of interaction have to be explicitly handled by all parties to these interactions). This is simply not the case for standard threads-and-locks concurrency, which have no formal denotational semantics and by which we get surprised all the time.
However, we need some extensions to describe certain new dynamics - and this is where we turn to the pi-calculus. Specifically, we want to allow networks of processes to evolve, to change their topologies, to cope with growth and decay without losing semantic or structural integrity. We want to address the mobility of processes, channels and data and understand the relationships between these ideas. We want to retain the ability to reason about such systems, preserving the concept of refinement.
This version of the occam compiler supports the new occam-pi version of the language. New features include:
More information relating to the new langauge extensions for occam-pi. Additional information on KRoC, including a reference manual (currently mostly occam, not occam-pi), standards for the new occamdoc tool, development notes and other can be found on the Programming Languages and Systems Group Wiki.
The open-source version of KRoC is available as a tarball:
14/01/2006: KRoC 1.4.0 latest stable version (Linux/i386, FreeBSD/i386, Cygwin/i386):
kroc-1.4.0.tar.gz (6.67 M), kroc-1.4.0.tar.bz2 (4.20 M)
Note: This version is now quite old. If you intend to use the newer features of the language, we'd recommend you follow the instructions here, to install a newer version of KRoC.
Once downloaded, unpack the tarball, change into the `kroc-version' directory and run the `build' script to compile and install KRoC:
bash$ tar -xvzf kroc-1.4.0.tar.gz
kroc-1.4.0/
kroc-1.4.0/build
...
bash$ cd kroc-1.4.0
bash$ ./build
KRoC installation configuration
... configuration options ...
1-7 to change path, A-E to toggle/set feature, Ctrl-C to abort,
return to confirm and install:
... output from build ...
By default, KRoC will install itself in the source-tree. To select a different installation directory, enter 1 at the prompt, and when prompted again, type the desired directory. Other parts of the configuration may be set in a similar way. To install with the default settings, simply press return. The build process can be aborted at any time by pressing Ctrl-C -- when `build' is re-run, it will not re-build things that are already compiled. For detailed information on building KRoC:
bash$ ./build --help
... build usage and options ...
Note: if the installation completes successfully, the `build' script will display a message -- read this carefully as it contains important information relating to the package. You should also read the top-level `README' file.
The various example programs can be built with:
bash$ ./build examples
... output from build ...
Example programs are now installed under the 'kroc specific files' directory (as given in the configuration). Currently these are:
| Directory | Description |
| examples/course/ | course library example programs, demos and some model answers to occam exercises |
| examples/syncs/ | synchronisation primitive examples |
| examples/udc/ | user-defined channel example programs |
| examples/cif/ | C-interface example programs |
| examples/demos/ | the `better-bar' demonstrator |
| examples/bsc/ | file/socket/process examples (for blocking sys-calls) |
| examples/dynproc/ | dynamically loadable process examples |
| examples/sdlraster/ | SDLRaster example programs |
The source-tree can be cleaned by running `./build clean'. This will not remove anything already installed, but will remove any example programs and cgtests built (that are built using `./build examples' and `./build cgtests' respectively).
Much of the KRoC documentation is provided in the form of text/HTML files and UNIX manual pages. In KRoC 1.3.3 and above, the standard "course" library is documented by manpages, in addition to minimal manpages for the Inmos libraries (that just detail the PROC/FUNCTION interfaces and give a brief description of the library). Documentation relating to KRoC is installed in the specified 'kroc specific files' directory under doc/.
If you're new to KRoC, you should read the Getting started with KRoC page (a textual version is included in the distribution as essentially-kroc.txt). This describes the basics of occam-pi programs and how to compile them with KRoC.
The following documentation is on-line (and also included in the distribution):
If you have problems compiling or installing KRoC on your Linux system, we may be able to help. When the `build' script is run, it leaves a copy of its output in a file called `typescript' (left in the top-level directory of the distribution). If the compilation fails, this file will have a copy of the error-message. E-mail this file as an attachment to ofa-bugs@kent.ac.uk. Please also include in the email any relevant information, e.g.: hardware/processor (`cat /proc/cpuinfo'); the Linux kernel version (`cat /proc/version', or `uname -a); and the name and version of the distribution you are using (e.g. ``Debian stable'').
It is often helpful to have a full typescript file. To get this, `distclean' then re-build the distribution:
bash$ ./build distclean
... output from build ...
bash$ ./build
KRoC installation configuration
... configuration options ...
1-7 to change path, A-E to toggle/set feature, Ctrl-C to abort,
return to confirm and install:
... output from build ...
There is a mailing-list for the dicussion of occam/KRoC related issues, occam-com@kent.ac.uk. This is a closed list, to subscribe please mail Peter Welch.
The KRoC open-source release is under continuous development. The following additions/extensions are planned for future releases, and may already be partially supported in the development releases:
All publications relating to the KRoC project can be found on this page: http://www.cs.kent.ac.uk/research/groups/sys/kroc.html.
|
Last modified 3rd March 2013 |
