🚀 go-pugleaf

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!)

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

From: 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 elektro- og datateknikk},
  year = "1993",
  
  address = {N-7000 Trondheim, Norway},
  month = apr,
  note = "Title and date are not final.",
  type = "Hovedoppgave",
}
 
--------------------------------------------------------------------------------------

From: "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.

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

From: 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: ]]

From: 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: ]]

From: 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 ]]

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

From: 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.
\newblock {\em {A Theorem Prover for UNITY in Higher Order Logic}}.
\newblock PhD thesis, Technical University of Denmark, March 1992.

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

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

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

From: 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 !

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

From: "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.

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

From: 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 ]]

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

From: 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 ]]

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

From: 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?

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

From: 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

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

From: "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 ]]

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

From: 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

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

From: 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.

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

From: 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)            | Whenever you 
Institut fuer Programmstrukturen und Datenorganisation  | complicate things,
Universitaet Karlsruhe;  D-7500 Karlsruhe 1;  Germany   | they get
(Voice: ++49/721/608-4068, FAX: ++49/721/694092)        | less simple.