SUMMARY: UNITY implementations

Quite a while back (November 1992) I posted the following request for
information:


------------------------------------------------------------------------------
      Does anybody know about implementations of the UNITY language ?
      Especially parallel ones ?


      We have built a translator from UNITY into MPL on the MasPar and
      I am looking for comparable systems (but also sequential ones).


      All pointers and short descriptions are welcome.
------------------------------------------------------------------------------


Our software (mentioned in the reply above) which only works for MasPar
MP-1 and MP-2 SIMD computers, is available for anonymous ftp from


      SanFrancisco.ira.uka.de [129.13.13.110]
      in directory /pub/maspar as maspar_unity.tar.Z (154 kB)


This is the summary of the replies I received on my request.
The reason why it comes so late is that
(a) replies dropped in quite slowly
(b) I had some additional interaction with some people
(c) this is still not complete (but now I give up).


Summing up, I must admit that not very much useful information has shown up.


Here are the main parts of the individual replies:
(Two german colleagues replied in German. Sorry!)


------------------------------------------------------------------------------


Reply-To: Andreas Eide <eide@fzi.de>
Date: Fri, 13 Nov 92 9:34:11 GMT


I am a Norwegian student currently writing my diploma thesis here in
Karlsruhe. I'm with the group Systementwurf in der Mikroelektronik at FZI.
I've just started out.


The subject of my thesis is partitioning of UNITY descriptions on MIMD
architectures. It appears to me that your work might be of interest to
me.


I would be very grateful for any references to your work. I would also be
grateful for any references on UNITY.


[[ I asked for the title of his thesis and got: ]]


I supply the bibtex entry of my diploma
thesis. Please note that the title is not final, and is verly likely
to change.


@MASTERSTHESIS{Eide93,
    author = {Andreas Eide},
    title = {Partitioning of UNITY Descriptions on MIMD Architectures},
    school = {Norges Tekniske H{\o}gskole, Avdeling for elektroog datateknikk},
    year = "1993",


    address = {N-7000 Trondheim, Norway},
    month = apr,
    note = "Title and date are not final.",
    type = "Hovedoppgave",
}


------------------------------------------------------------------------------


Reply-To: "J. Staunstrup" <jst@id.dth.dk>


We have several translators transforming a language called Synchronized
Transitions (many similarities with UNITY) to C and to various circuit
realizations (certainly parallel). Several papers have been published.


[[ I asked for the references and got: ]]


@article{Staunstrup88,
    author = "J\o{}rgen Staunstrup and Mark R. Greenstreet",
    title = "From High-Level Descriptions to {VLSI} Circuits",
    journal = "{BIT}",
    year = 1988,
    pages = "620-638",
    volume = 28,
    number = 3
}
@inproceedings{hawaii,
    author = "Mark Greenstreet and Kai Li and J{\o}rgen Staunstrup",
    title = "Synchronized Transitions on Multiprocessors",
    booktitle = "HICSS-22",
    publisher = "IEEE",
p year = 1989
}
@incollection{st90,
    author = "J\o{}rgen Staunstrup and Mark Greenstreet",
    title = "{Synchronized Transitions}",
    booktitle = "Formal Methods for {VLSI} Design",
    editor = "J\o{}rgen Staunstrup",
    year = 1990,
    pages = "71-128",
    publisher = "North-Holland/Elsevier"
}
@inproceedings{Staunstrup91,
    author = "Per H. Christensen and Henrik Hulgaard and J{\o}rgen
     Staunstrup",
    title = "Synthesis of Delay Insensitive Circuits from Verified
     Programs",
    booktitle = "Research directions in high-level parallel programming
     languages",
    editor = "J.-P. Banatre and D. Le Metayer",
    year = "1992",
    publisher = "Springer Lecture Notes 574",
    pages = "326-337"
}


I recommend that you start with st90.


------------------------------------------------------------------------------


Reply-To: nbm@epcc.edinburgh.ac.uk


Dave DeRoure at the University of Southampton did some work on a Unity
implementation on, I think, a transputer based machine.


I'm afraid I don't have an email address handy, but if you are interested
I can try to dig one out for you.


[[ and a similar one: ]]


Reply-To: Catherine Barnaby <cath@inmos.co.uk>


I'm not sure if this is of interest to you...


David DeRoure at Southampton University did some work with UNITY as a part
of the ESPRIT project PUMA.


Off the top of my head it was looking at the use of UNITY for programming
PRAM-type machines.


Davids' e-mail is (or was)
D.DeRoure@ecs.soton.ac.uk


I suggest you contact him directly: I don't even know if he still works in
the area. If you have problems, contact me again and I'll try and sort
them out. I'm rather busy, so it may take some time.


[[ I contacted DeRoure and got: ]]


Reply-To: Dave De Roure <D.C.DeRoure@ecs.southampton.ac.uk>


I was responsible for some UNITY work within an ESPRIT project (PUMA). It
was in a programming languages workpackage, which include BSP-occam,
fortran, ML and UNITY. This meant that the UNITY work was seen as a very
high level programming language, and packaged as such - there is a
compiler (written in EuLisp) which targets to the common back-end of the
project (BSP-occam). I wasn't altogether happy with this way of using
UNITY, but it's turned out to be a useful tool in the sense of an
executable specification language.


I have some documents from the PUMA project describing the UNITY work -
can you collect them if I make them available by ftp, or would you prefer
me to post them?


Let me know how you get on. I've not been able to follow up the UNITY
work per se, but I'm using many of the ideas in other work so I'm still
interested.


[[ I requested to get the documents, but did not get any answer ]]


------------------------------------------------------------------------------


Reply-To: Flemming Andersen <fa@tfl.dk>


I have implemented the UNITY theory in a general theorem proving system
called HOL. The HOL prover is implemented at the University of Cambridge.
The socalled HOL-UNITY implementation was made as part of my PhD thesis.
It is a formalization of the UNITY theory as described in Chandy and
Misra's book.


However, HOL-UNITY is not a compiler but a verification tool.


The HOL-UNITY theory is now being used for proving properties of parallel
programs. The user interface is however still for experts-only. Hence,
it is planned to extend HOL-UNITY to support automated proof techniques
and a programming language.


The goal of working with a general theorem prover like HOL is to develop
tools in a safe way. Tools that are by default proved correct and which
are hopefully going to be used for verifying (at least parts of) software
mainly within the area of telecommunication.


[[ I asked for references and whether HOL-UNITY does only reason about
      or does also execute UNITY. I got: ]]


Currently no execution is directly supported, but at the last HOL'93
Workshop it was told that people are working on tools for executing HOL
terms. However, we have planned to make a simple interpreter for the
UNITY programming language as part of the interface work on HOL-UNITY.


HOL-UNITY is available as a library in the next version 2.1 of HOL system
and the HOL system is public domain software.




Here are some (LaTeX/BibTeX) references:


\bibitem[And92]{FA92}
Flemming Andersen.
  {\em {A Theorem Prover for UNITY in Higher Order Logic}}.
  PhD thesis, Technical University of Denmark, March 1992.


\bibitem[And92b]{FA92a}
Flemming Andersen.
  {A Theory for UNITY in The Cambridge HOL System}.
  {TFL LD 1992-9}, TFL - Telecommunications Research Laboratory, March
    1992.


\bibitem[AP91]{FAKDP91}
Flemming Andersen and Kim~Dam Petersen.
  {Recursive Boolean Functions in HOL}.
  In {\em {1991 International Workshop on the HOL Theorem Proving
    System and its Applications}}, pages 367--377. IEEE Computer Society, August
    1991.


------------------------------------------------------------------------------


Reply-To: Syst{ Kari <ks@karikukko.cs.tut.fi>
Date: Fri, 13 Nov 92 16:00:25 +0200


One was published in Comp. Lang. Vol 18., No1. pp 17-30, 1993
Radha,Muthukrishnan: A Portable implentation of Unity on von Neuman
Machines.


[[ The date given for 'was published' was inconsistent with reality.
    So I asked: ]]


> > One was published in Comp. Lang. Vol 18., No1. pp 17-30, 1993
> ^^^ ^^^^
> WAS published ? Or will be ?
> And what is the full name of that journal ?


Hmm... I have a xerox copy of the article. On the left-side corder there
is 1993 but on the right hand corner "Copyright 1992, Pergmon Press.


Anyway it seems that it is already published !


------------------------------------------------------------------------------


Reply-To: "Dr. Franz Kurfess" <franz@neuro.informatik.uni-ulm.de>


I don't know of any Unity implementations, but I used Unity extensively in
my PhD thesis "Parallelism in Logic -- Its Potential for Performance and
Program Development" Vieweg Verlag, Braunschweig, 1991.


------------------------------------------------------------------------------


Reply-To: filali@irit.fr


I work on UNITY. I would be very interested by the work you have done with
UNITY and MPL.


[[ I cried 'MORE INFORMATION' but did not get something concrete ]]


------------------------------------------------------------------------------


Reply-To: Jayadev Misra <misra@cs.utexas.edu>


I have forwarded your request to Allen Emerson for information about
implementations of UNITY to two people (Rajive Bagrodia and Flemming
Andersen) who should be able to give you some pointers.


I would be interested in reading about your UNITY implementation if you
have a manual.


[[ Later I received some pointers from Mani Chandy, see below ]]


------------------------------------------------------------------------------


Reply-To: BAGGETT WILLIAM B <BAGGETTW@memstvx1.memst.edu>


Please let me know about the response you received to your question about
UNITY implementations. I am reading the textbook for a class I am taking
this semester. I could work on a sequential implementation for a class
project, but I would like to know what is already out there. Is your
translator to MPL available?


------------------------------------------------------------------------------


Reply-To: Arnulf Mester <mester@ls4dec4.informatik.uni-dortmund.de>


Aus dem hohlen Bauch heraus faellt mir die Program Composition Motation
(PCN, von C. oder M., historisch nach UNITY) ein, zu deren Lehre auch ein
Werkzeug entwickelt worden sein soll.


Ausserdem existiert irgendwo im Mittelsueden (Saarbruecken?) eine UNITY
Interpreter Implementierung.


Da ich privat gerade umziehe, komme ich nicht an die Unterlagen. Bei
Interesse bitte in zwei Wochen nochmal kurz anmailen - dann kann ich sie
raussuchen.


[[ and a later mail included: ]]


H. Peter Gumm, MUNITY
Uni Marburg, Informatik, 14 S.
wahrscheinlich weniger von Interesse, zielt in Richtung Goldschlag
beschreibt einen interactive verifier for UNITY programs
Papier vom GI/ITG Workshop der FG KUVS Magdeburg April? 92


------------------------------------------------------------------------------


Reply-To: "K. Mani Chandy" <mani@vlsi.cs.caltech.edu>


I have heard that the following people were working on UNITY
implementations, but you should check with them directly.


Bill Mayne
9707 Lawndale Dr.
Silver Spring
MD 20901.


Bill Mayne
9707 Lawndale Dr.
Silver Spring
MD 20901.


UNITY at U.B.C.
Alan Wagner
University of British Columbia,
Computer Science Department,
Vancouver,
British Columbia,
Canada,
electronic mail:wagner@cs.ubc.ca


Prof. James C. Browne,
Computer Science Department,
Taylor Hall,
University of Texas,
Austin, Texas 78712-1188,


Dr. Andre Stern,
Oxford University Computing Lab,
Programming Research Group,
8-11 Keble Road,
Oxford OX1 3QD,
UNITED KINGDOM, electronic-mail:
stern%prg.oxford.ac.uk@NSFnet-Relay.AC.UK


Dr. Filali Mamoun,
Chercheur CNRS,
Laboratoire LSI-IRIT,
Universite Paul Sabatier,
F-31062 Toulose Cedex,
France.


Arnulf Mester
University of Dortmund, Dept. of Computer Science
IRB
POB. 500 500, D-4600 Dortmund 50, West Germany
e-mail: am@heike.informatik.uni-dortmund.de


Mr. Edgar Lederer
Institut fur Informatik der Universitat Zurich
Winterthurerstrasse 190
CH-8057 Zurich
Switzerland


Frank Bieler <bieler@karlsruhe.gmd.dbp.de>


[[ I tried to contact these people, the results are below ]]


------------------------------------------------------------------------------


Reply-To: bieler@karlsruhe.gmd.de


Ja, ganz recht, ich habe mich mal mit UNITY beschaeftigt. Ist schon ein
paar Jahre her. Ich habe fuer die Programmnotation von UNITY einen
Compiler geschrieben, der ein UNITY-Programm in eine Zwischendarstellung
uebersetzt. Diese wird dann von einem sequentiellen Interpreter
abgearbeitet. Den Fixpunkt eines Programms habe ich mit einer
Schattenspeicher-Technik festgestellt (Speicher verdoppelt und verglichen,
ob sich was veraendert hat).


Das alles ist aber nicht mehr in Gebrauch. Ich habe den ganzen Kram Edgar
Knapp zur Verfuegung gestellt (Mitarbeiter von Misra). Der wollte einen
Proof-Checker bauen und mein Frontend verwenden. ich weiss aber nicht, was
sich daraus entwickelt hat.


Als Literatur kann ich Dir nur ein internes Papier von mir geben


------------------------------------------------------------------------------


Reply-To: Alan Wagner <wagner@cs.ubc.ca>


I am still very interested in UNITY, unfortunately we have had very little
opportunity to look at it in any detail.


------------------------------------------------------------------------------


Reply-To: Syed Irfan Hyder <hyder@cs.utexas.edu>


Look for K. Mani Chandy's work on PCN. I think it is some kind of
implementation of Unity.


Send mail to gouda@cs.utexas.edu or misra@cs.utexas.edu


Both teach the book on unity.


------------------------------------------------------------------------------


That's all folks


    Lutz


Lutz Prechelt (email: prechelt@ira.uka.de)
Institut fuer Programmstrukturen und Datenorganisation
Universitaet Karlsruhe; D-7500 Karlsruhe 1; Germany
(Voice: ++49/721/608-4068, FAX: ++49/721/694092)
--

Return to the comp.compilers page.
Search the comp.compilers archives again.