home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #3 / NN_1993_3.iso / spool / comp / parallel / 3031 < prev    next >
Encoding:
Text File  |  1993-01-22  |  16.0 KB  |  434 lines
  1. Newsgroups: comp.parallel
  2. Path: sparky!uunet!destroyer!gatech!hubcap!fpst
  3. From: Lutz Prechelt <prechelt@ira.uka.de>
  4. Subject: SUMMARY: UNITY implementations
  5. Message-ID: <1993Jan22.161525.21882@hubcap.clemson.edu>
  6. Keywords: verification, specification
  7. Sender: newsadm@ira.uka.de
  8. Nntp-Posting-Host: i41s18.ira.uka.de
  9. Organization: University of Karlsruhe, FRG
  10. Date:     Fri, 22 Jan 1993 16:00:32 +0100
  11. Approved: parallel@hubcap.clemson.edu
  12. Lines: 420
  13.  
  14.  
  15. Quite a while back (November 1992) I posted the following request for information:
  16.  
  17. ------------------------------------------------------------------------------------
  18.    Does anybody know about implementations of the UNITY language ?
  19.    Especially parallel ones ?
  20.  
  21.    We have built a translator from UNITY into MPL on the MasPar and
  22.    I am looking for comparable systems (but also sequential ones).
  23.  
  24.    All pointers and short descriptions are welcome.
  25. ------------------------------------------------------------------------------------
  26.  
  27. Our software (mentioned in the reply above) which only works for MasPar MP-1
  28. and MP-2 SIMD computers, is available for anonymous ftp from
  29.  
  30.    SanFrancisco.ira.uka.de [129.13.13.110]
  31.    in directory /pub/maspar as  maspar_unity.tar.Z (154 kB)
  32.  
  33.  
  34. This is the summary of the replies I received on my request.
  35. The reason why it comes so late is that 
  36. (a) replies dropped in quite slowly
  37. (b) I had some additional interaction with some people
  38. (c) this is still not complete (but now I give up).
  39.  
  40. Summing up, I must admit that not very much useful information has shown up.
  41.  
  42. Here are the main parts of the individual replies:
  43. (Two german colleagues replied in German. Sorry!)
  44.  
  45. --------------------------------------------------------------------------------------
  46. --------------------------------------------------------------------------------------
  47.  
  48. From: Andreas Eide <eide@fzi.de>
  49. Date: Fri, 13 Nov 92 9:34:11 GMT
  50.  
  51. I am a Norwegian student currently writing my diploma thesis here in
  52. Karlsruhe. I'm with the group Systementwurf in der Mikroelektronik at
  53. FZI. I've just started out. 
  54.  
  55. The subject of my thesis is partitioning of UNITY descriptions on MIMD
  56. architectures.  It appears to me that your work might be of interest
  57. to me.
  58.  
  59. I would be very grateful for any references to your work. I would also
  60. be grateful for any references on UNITY.
  61.  
  62. [[ I asked for the title of his thesis and got: ]]
  63.  
  64. I supply the bibtex entry of my diploma
  65. thesis. Please note that the title is not final, and is verly likely
  66. to change.
  67.  
  68. @MASTERSTHESIS{Eide93,
  69.   author = {Andreas Eide},
  70.   title = {Partitioning of UNITY Descriptions on MIMD Architectures},
  71.   school  = {Norges Tekniske H{\o}gskole, Avdeling for elektro- og datateknikk},
  72.   year = "1993",
  73.   
  74.   address = {N-7000 Trondheim, Norway},
  75.   month = apr,
  76.   note = "Title and date are not final.",
  77.   type = "Hovedoppgave",
  78. }
  79.  
  80. --------------------------------------------------------------------------------------
  81.  
  82. From: "J. Staunstrup" <jst@id.dth.dk>
  83.  
  84. We have several translators transforming a language called Synchronized
  85. Transitions (many similarities with UNITY) to C and to various
  86. circuit realizations (certainly parallel). Several papers have been
  87. published.
  88.  
  89. [[ I asked for the references and got: ]]
  90.  
  91. @article{Staunstrup88,
  92.   author        = "J\o{}rgen Staunstrup and Mark R. Greenstreet",
  93.   title         = "From High-Level Descriptions to {VLSI} Circuits",
  94.   journal       = "{BIT}",
  95.   year          = 1988,
  96.   pages         = "620-638",
  97.   volume        = 28,
  98.   number        = 3
  99. }
  100. @inproceedings{hawaii,
  101.   author        = "Mark Greenstreet and Kai Li and J{\o}rgen Staunstrup",
  102.   title         = "Synchronized Transitions on Multiprocessors",
  103.   booktitle     = "HICSS-22",
  104.   publisher     = "IEEE",
  105. p  year          = 1989
  106. }
  107. @incollection{st90,
  108.   author        = "J\o{}rgen Staunstrup and Mark Greenstreet",
  109.   title         = "{Synchronized Transitions}",
  110.   booktitle     = "Formal Methods for {VLSI} Design",
  111.   editor        = "J\o{}rgen Staunstrup",
  112.   year          = 1990,
  113.   pages         = "71-128",
  114.   publisher     = "North-Holland/Elsevier"
  115. }
  116. @inproceedings{Staunstrup91,
  117.   author     = "Per H. Christensen and Henrik Hulgaard and J{\o}rgen Staunstrup",
  118.   title      = "Synthesis of Delay Insensitive Circuits from Verified Programs",
  119.   booktitle  = "Research directions in high-level parallel programming languages",
  120.   editor     = "J.-P. Banatre and D. Le Metayer",
  121.   year       = "1992",
  122.   publisher  = "Springer Lecture Notes 574",
  123.   pages      = "326-337"
  124. }
  125.  
  126. I recommend that you start with st90.
  127.  
  128. --------------------------------------------------------------------------------------
  129.  
  130. From: nbm@epcc.edinburgh.ac.uk
  131.  
  132. Dave DeRoure at the University of Southampton did some work on a 
  133. Unity implementation on, I think, a transputer based machine.  
  134.  
  135. I'm afraid I don't have an email address handy, but if you are 
  136. interested I can try to dig one out for you.
  137.  
  138. [[ and a similar one: ]]
  139.  
  140. From: Catherine Barnaby <cath@inmos.co.uk>
  141.  
  142. I'm not sure if this is of interest to you...
  143.  
  144. David DeRoure at Southampton University did some work 
  145. with UNITY as a part of the ESPRIT project PUMA. 
  146.  
  147. Off the top of my head it was looking at 
  148. the use of UNITY for programming PRAM-type machines.
  149.  
  150. Davids' e-mail is (or was) 
  151. D.DeRoure@ecs.soton.ac.uk
  152.  
  153. I suggest you contact him directly: I don't even know if he 
  154. still works in the area. If you have problems, contact me again
  155. and I'll try and sort them out. I'm rather busy, so it may
  156. take some time.
  157.  
  158. [[ I contacted DeRoure and got: ]]
  159.  
  160. From: Dave De Roure <D.C.DeRoure@ecs.southampton.ac.uk>
  161.  
  162. I was responsible for some UNITY work within an ESPRIT project (PUMA).
  163. It was in a programming languages workpackage, which include BSP-occam,
  164. fortran, ML and UNITY.  This meant that the UNITY work was seen as a
  165. very high level programming language, and packaged as such - there is
  166. a compiler (written in EuLisp) which targets to the common back-end of
  167. the project (BSP-occam).  I wasn't altogether happy with this way
  168. of using UNITY, but it's turned out to be a useful tool in the sense
  169. of an executable specification language.
  170.  
  171. I have some documents from the PUMA project describing the UNITY work - can 
  172. you collect them if I make them available by ftp, or would you prefer me 
  173. to post them?
  174.  
  175. Let me know how you get on.  I've not been able to
  176. follow up the UNITY work per se, but I'm using many of the ideas in
  177. other work so I'm still interested.
  178.  
  179. [[ I requested to get the documents, but did not get any answer ]]
  180.  
  181. --------------------------------------------------------------------------------------
  182.  
  183. From: Flemming Andersen <fa@tfl.dk>
  184.  
  185. I have implemented the UNITY theory in a general theorem proving system
  186. called HOL.  The HOL prover is implemented at the University of Cambridge.  The
  187. socalled HOL-UNITY implementation was made as part of my PhD thesis.  It is a
  188. formalization of the UNITY theory as described in Chandy and Misra's book.
  189.  
  190. However, HOL-UNITY is not a compiler but a verification tool.
  191.  
  192. The HOL-UNITY theory is now being used for proving properties of parallel
  193. programs.  The user interface is however still for experts-only.  Hence, it is
  194. planned to extend HOL-UNITY to support automated proof techniques and a
  195. programming language.
  196.  
  197. The goal of working with a general theorem prover like HOL is to develop tools
  198. in a safe way.  Tools that are by default proved correct and which are
  199. hopefully going to be used for verifying (at least parts of) software mainly
  200. within the area of telecommunication.
  201.  
  202. [[ I asked for references and whether HOL-UNITY does only reason about
  203.    or does also execute UNITY. I got: ]]
  204.  
  205. Currently no execution is directly supported, but at the last HOL'93
  206. Workshop it was told that people are working on tools for executing
  207. HOL terms.  However, we have planned to make a simple interpreter for
  208. the UNITY programming language as part of the interface work on
  209. HOL-UNITY.
  210.  
  211. HOL-UNITY is available as a library in the next version 2.1 of HOL
  212. system and the HOL system is public domain software.
  213.  
  214.  
  215. Here are some (LaTeX/BibTeX) references:
  216.  
  217. \bibitem[And92]{FA92}
  218. Flemming Andersen.
  219. \newblock {\em {A Theorem Prover for UNITY in Higher Order Logic}}.
  220. \newblock PhD thesis, Technical University of Denmark, March 1992.
  221.  
  222. \bibitem[And92b]{FA92a}
  223. Flemming Andersen.
  224. \newblock {A Theory for UNITY in The Cambridge HOL System}.
  225. \newblock {TFL LD 1992-9}, TFL - Telecommunications Research Laboratory, March
  226.   1992.
  227.  
  228. \bibitem[AP91]{FAKDP91}
  229. Flemming Andersen and Kim~Dam Petersen.
  230. \newblock {Recursive Boolean Functions in HOL}.
  231. \newblock In {\em {1991 International Workshop on the HOL Theorem Proving
  232.   System and its Applications}}, pages 367--377. IEEE Computer Society, August
  233.   1991.
  234.  
  235. --------------------------------------------------------------------------------------
  236.  
  237. From: Syst{ Kari <ks@karikukko.cs.tut.fi>
  238. Date: Fri, 13 Nov 92 16:00:25 +0200
  239.  
  240. One was published in Comp. Lang. Vol 18., No1. pp 17-30, 1993
  241. Radha,Muthukrishnan: A Portable implentation of Unity on von Neuman Machines.
  242.  
  243. [[ The date given for 'was published' was inconsistent with reality.
  244.   So I asked: ]]
  245.  
  246. > > One was published in Comp. Lang. Vol 18., No1. pp 17-30, 1993
  247. >       ^^^                                                  ^^^^
  248. > WAS published ?  Or will be ?
  249. > And what is the full name of that journal ?
  250.  
  251. Hmm... I have a xerox copy of the article. On the left-side corder there
  252. is 1993 but on the right hand corner "Copyright 1992, Pergmon Press.
  253.  
  254. Anyway it seems that it is already published !
  255.  
  256. --------------------------------------------------------------------------------------
  257.  
  258. From: "Dr. Franz Kurfess" <franz@neuro.informatik.uni-ulm.de>
  259.  
  260. I don't know of any Unity implementations,
  261. but I used Unity extensively in my PhD thesis
  262. "Parallelism in Logic -- Its Potential for Performance and Program Development"
  263. Vieweg Verlag, Braunschweig, 1991.
  264.  
  265. --------------------------------------------------------------------------------------
  266.  
  267. From: filali@irit.fr
  268.  
  269. I work on UNITY. I would be very interested by the
  270. work you have done with UNITY and MPL.
  271.  
  272. [[ I cried 'MORE INFORMATION' but did not get something concrete ]]
  273.  
  274. --------------------------------------------------------------------------------------
  275.  
  276. From: Jayadev Misra <misra@cs.utexas.edu>
  277.  
  278. I have forwarded your request to Allen Emerson for information about
  279. implementations of UNITY to two people (Rajive Bagrodia and Flemming Andersen)
  280. who should be able to give you some pointers.
  281.  
  282. I would be interested in reading about your UNITY implementation if you have
  283. a manual.
  284.  
  285. [[ Later I received some pointers from Mani Chandy, see below ]]
  286.  
  287. --------------------------------------------------------------------------------------
  288.  
  289. From: BAGGETT WILLIAM B <BAGGETTW@memstvx1.memst.edu>
  290.  
  291. Please let me know about the response you received to your question
  292. about UNITY implementations.  I am reading the textbook for a class I am
  293. taking this semester.  I could work on a sequential implementation for
  294. a class project, but I would like to know what is already out there.  Is
  295. your translator to MPL available?
  296.  
  297. --------------------------------------------------------------------------------------
  298.  
  299. From: Arnulf Mester <mester@ls4dec4.informatik.uni-dortmund.de>
  300.  
  301. Aus dem hohlen Bauch heraus faellt mir die
  302. Program Composition Motation (PCN, von C. oder M., historisch nach UNITY)
  303. ein, zu deren Lehre auch ein Werkzeug entwickelt worden sein soll.
  304.  
  305. Ausserdem existiert irgendwo im Mittelsueden (Saarbruecken?)
  306. eine UNITY Interpreter Implementierung.
  307.  
  308. Da ich privat gerade umziehe, komme ich nicht an die Unterlagen.
  309. Bei Interesse bitte in zwei Wochen nochmal kurz anmailen - dann kann ich
  310. sie raussuchen.
  311.  
  312. [[ and a later mail included: ]]
  313.  
  314. H. Peter Gumm, MUNITY
  315. Uni Marburg, Informatik, 14 S.
  316.     wahrscheinlich weniger von Interesse, zielt in Richtung Goldschlag
  317.     beschreibt einen interactive verifier for UNITY programs
  318.     Papier vom GI/ITG Workshop der FG KUVS Magdeburg April? 92
  319.  
  320. --------------------------------------------------------------------------------------
  321.  
  322. From: "K. Mani Chandy" <mani@vlsi.cs.caltech.edu>
  323.  
  324. I have heard that the following people were working on UNITY
  325. implementations, but you should check with them directly.
  326.  
  327.                        Bill Mayne
  328.                        9707 Lawndale Dr.
  329.                        Silver Spring
  330.                        MD 20901.
  331.  
  332.                        Bill Mayne
  333.                        9707 Lawndale Dr.
  334.                        Silver Spring
  335.                        MD 20901.
  336.                       
  337.                        UNITY at U.B.C.
  338.                        Alan Wagner
  339.                        University of British Columbia, 
  340.                        Computer Science Department, 
  341.                        Vancouver, 
  342.                        British Columbia, 
  343.                        Canada,
  344.                        electronic mail:wagner@cs.ubc.ca
  345.                        
  346.                        Prof. James C. Browne, 
  347.                        Computer Science Department,
  348.                        Taylor Hall, 
  349.                        University of Texas, 
  350.                        Austin, Texas 78712-1188,
  351.                        
  352.                        Dr. Andre Stern,
  353.                        Oxford University Computing Lab,
  354.                        Programming Research Group,
  355.                        8-11 Keble Road,
  356.                        Oxford OX1 3QD,
  357.                        UNITED KINGDOM, electronic-mail:
  358.                        stern%prg.oxford.ac.uk@NSFnet-Relay.AC.UK
  359.                        
  360.                        Dr. Filali Mamoun,
  361.                        Chercheur CNRS,
  362.                        Laboratoire LSI-IRIT,
  363.                        Universite Paul Sabatier,
  364.                        F-31062 Toulose Cedex,
  365.                        France.
  366.                        
  367.                        Arnulf Mester
  368.                        University of Dortmund, Dept. of Computer Science
  369.                        IRB      
  370.                        POB. 500 500, D-4600 Dortmund 50, West Germany
  371.                        e-mail: am@heike.informatik.uni-dortmund.de
  372.  
  373.                        Mr. Edgar Lederer
  374.                        Institut fur Informatik der Universitat Zurich
  375.                        Winterthurerstrasse 190
  376.                        CH-8057 Zurich
  377.                        Switzerland
  378.  
  379.                        Frank Bieler <bieler@karlsruhe.gmd.dbp.de>
  380.  
  381. [[ I tried to contact these people, the results are below ]]
  382.  
  383. --------------------------------------------------------------------------------------
  384.  
  385. From: bieler@karlsruhe.gmd.de
  386.  
  387. Ja, ganz recht, ich habe mich mal mit UNITY beschaeftigt. Ist schon 
  388. ein paar Jahre her. Ich habe fuer die Programmnotation von UNITY
  389. einen Compiler geschrieben, der ein UNITY-Programm in eine
  390. Zwischendarstellung uebersetzt. Diese wird dann von einem
  391. sequentiellen Interpreter abgearbeitet. Den Fixpunkt eines Programms
  392. habe ich mit einer Schattenspeicher-Technik festgestellt (Speicher
  393. verdoppelt und verglichen, ob sich was veraendert hat). 
  394.  
  395. Das alles ist aber nicht mehr in Gebrauch. Ich habe den ganzen Kram
  396. Edgar Knapp zur Verfuegung gestellt (Mitarbeiter von Misra). Der
  397. wollte einen Proof-Checker bauen und mein Frontend verwenden. ich
  398. weiss aber nicht, was sich daraus entwickelt hat.
  399.  
  400. Als Literatur kann ich Dir nur ein internes Papier von mir geben
  401.  
  402. --------------------------------------------------------------------------------------
  403.  
  404. From: Alan Wagner <wagner@cs.ubc.ca>
  405.  
  406. I am still very interested in UNITY, unfortunately we
  407. have had very little opportunity to look at it in any
  408. detail.
  409.  
  410. --------------------------------------------------------------------------------------
  411.  
  412. From: Syed Irfan Hyder <hyder@cs.utexas.edu>
  413.  
  414. Look for K. Mani Chandy's work on PCN. I think it
  415. is some kind of implementation of Unity.
  416.  
  417. Send mail to gouda@cs.utexas.edu
  418. or misra@cs.utexas.edu
  419.  
  420. Both teach the book on unity.
  421.  
  422. --------------------------------------------------------------------------------------
  423. --------------------------------------------------------------------------------------
  424.  
  425. That's all folks
  426.  
  427.   Lutz
  428.  
  429. Lutz Prechelt   (email: prechelt@ira.uka.de)            | Whenever you 
  430. Institut fuer Programmstrukturen und Datenorganisation  | complicate things,
  431. Universitaet Karlsruhe;  D-7500 Karlsruhe 1;  Germany   | they get
  432. (Voice: ++49/721/608-4068, FAX: ++49/721/694092)        | less simple.
  433.  
  434.