La Macchina Universale.Vecchie idee e nuove applicazioni.

Alberto PolicritiDipartimento di Matematica e Informatica,

Universita’ di Udine.

The Universal ComputerThe road from Leibniz to Turing

Com’e’ nato il primo computer?

Ingredienti per un (significativo) passo avanti

• Una buona idea (una o piu’ persone geniali)• Un colpo di fortuna• Un mucchio di lavoro (un cospicuo numero di ingegneri)

Il colpo di fortuna

As Goldstine tells the story, von Neumann learned of the ENIAC project quite fortuitously

when the two met for the first time at a railway station during the summer of 1944. Von

Neumann soon joined the discussions with the ENIAC group at the Moore School.

------------------------------------Martin Davis 2000

Introduction

• If it should turn out that the basic logics of a machine designed for the numerical solution of differential equations coincide with the logics of a machine intended to make bills for a department store, I would regard this as the most amazing coincidence I have ever encountered. ---------------------------------------------Howard Aiken, 1956

• Let us now return to the analogy of the theoretical computing machines … It can be shown that a single special machine of that type can be made to do the work of all. It could in fact be made to work as a model of any other machine. The special machine may be called the universal machine. -----------------------------------------------Alan Turing 1947

Nell’autunno del 1945, quando l’ENIAC, la gigantesca calcolatrice contenente migliaia di valvole, era stata quasi completata presso la Moore School of Electrical Engineering a Philadelfia, un gruppo di esperti si incontrava regolarmente per discutere il disegno di

EDVAC, il suo possibile successore.

Le cose si complicarono quando, con immenso dispiacere di Eckert, il leader dei logici del gruppo, l’eminente matematico John von

Neumann, inizio’ a far circolare un draft report a suo nome relativo alla proposta di EDVAC che, concedendo poca

attenzione ai dettagli ingegneristici, gettava le basi progettuali logiche di quella che oggi chiamiamo l’architettura

di von Neumann.

Al passare delle settimane gli incontri diventavano via via piu’ acrimoniosi, e gli esperti che si dividevano in due gruppi iniziavano

a parlare di “ingegneri” e di “logici”. John Presper Eckert, leader degli ingegneri, era giustamente fiero dei risultati ottenuti con

ENIAC. Si pensava impossibile far funzionare 15.000 valvole insieme sufficientemente a lungo da ottenere qualcosa di utile. Tuttavia,

usando principi progettuali attenti e conservativi, Eckert era riuscito brillantemente in questa impresa.

Sebbene si potesse considerare un tour de force ingegneristico, ENIAC era logicamente un pasticcio. Solo

l’esperienza di logico di von Neumann---e quello che aveva imparato dal logico inglese Alan Turing---gli avevano

permesso di capire che una macchina per computare e’, in effetti, una macchina logica. I suoi circuiti incorporano il distillato di intuizioni di una significativa schiera di logici,

sviluppate nel corso di secoli.

Oggi, con l’avanzare impetuoso e continuo della tecnologia, mentre ammiriamo gli impressionanti risultati

ottenuti dagli ingegneri, e’ persino troppo facile dimenticare I logici le cui idee hanno reso tutto questo

possibile. Questo libro racconta la loro storia.

Chi ha inventato il Computer?(Chi ha parlato di macchina universale?)

• Joseph-Marie Jacquard (1752-1834)• Charles Babbage (1791-1871)• Ada Lovelace (1815-1852) “We may say most aptly that the

Analytical Engine weaves algebraic patterns just as the Jacquard-loom weaver flowers and leaves”

• Claude Shannon (1916-2001)• Howard Aiken (1900-1973)• John Atanasoff (1903-1995)• John Mauchly (1907-1980)• John Presper Eckert Jr. (1919-1995)• Herman Goldstine (1913-)• Earl R. Larson (1911-)

John Presper Eckert Jr. e John Mauchly

L’ENIAC

http://www.library.upenn.edu/special/gallery/mauchly/jwmintro.html

John W. Mauchly

and the Development of the ENIAC Computer

An Exhibition in the Department of Special Collections

Van Pelt Library, University of Pennsylvania

by Asaf Goldschmidt and Atsushi Akera

Department of History and Sociology of Science

University of Pennsylvania

In October 1973 Judge Earl Larson of the U.S. District Court in Minnesota rendered a decision invalidating the ENIAC patent. But rather than being a clear judgement as to who invented the electronic computer, this decision and the law suit, Honeywell v. Sperry-Rand, have done more to polarize opinions with respect to the varied contributions of many different individuals. In fact, this decision points to some of the limitations of the U.S. patent system with respect to complex technologies. Namely, the U.S. patent system sets forth certain pressures to name a sole inventor when invention itself is a often a highly collaborative process. We hope that this exhibition reveals something of the complexities involved in the process of invention. We hope also that in approaching the fifty-year mark of modern computing, we can recognize the diverse contributions of individuals, regardless of what we individually consider to be its origins.

ENIAC (e UNIVAC): l’impresa ingegneristica (e commerciale)

Jon von Neumann

Il contributo di von Neumann

In order to test the general applicability of the EDVAC, von Neumann wrote his first serious

program, not for the kind of number crunching application for which the machine was mainly

developed, but rather to simply sort data efficiently. The success of this program helped

to convince von Neumann that

``… it is legitimate to conclude already on the basis of the now available evidence, that the

EDVAC is very nearly an `all purpose‘ machine, and that the present principles for the logical

controls are sound.'‘------------------------------------John von Neumann

Alan Turinghttp://www.turing.org.uk/turing/

The Enigma

ACE: la risposta (inglese) di Turing ad Edvac

[It] is … very contrary to the line of development here, and much more in the

American tradition of solving one's difficulties by means of much equipment rather than by

thought.… Furthermore certain operations which we

regard as more fundamental than addition and multiplication have been omitted.

---------------------------------------------Alan Turing

[…] At the end of the Second World War, Britain's National Physics Laboratory (NPL) underwent a considerable expansion including a new Mathematics Division. J.R. Womersley (1907-1958), appointed head of this division, had seen the practical implications of Turing's 1936 Computable Numbers paper quite early on. […] On a visit to the United States in February 1945, he saw the ENIAC and obtained a copy of von Neumann's EDVAC Report. His reaction was to hire Alan Turing.

By the end of 1945, Turing had produced his remarkable ACE (Automatic Computing Engine) Report. One detailed comparison of the ACE Report with von Neumann's EDVAC Report, notes that whereas the latter ``is a draft and is unfinished … more important … is incomplete …'' the ACE Report ``is a complete description of a computer, right down to the logical circuit diagrams'' and even including ``a cost estimate of £11,200.''

La macchina ACE di Turing era molto diversa dall’EDVAC di von Neumann's (come lo erano I due matematici!).

Sebbene von Neumann volesse una macchina “all purpose” era molto piu’ portato a pensare a una grossa calcolatrice (number crunching).

L’idea di Turing era di costruire una macchina piu’ semplice e piu’ indipendente dalle possibli applicazioni.

[…] An opposing paradigm, the so-called RISC (reduced instruction set computing) architecture, adopted by a number of computer manufacturers, uses a minimal instruction set on the chip, with needed functionality supplied by programming, again very much in line with the ACE philosophy.

---------------------------------------------------------Martin Davis 2000

L’analisi di Turing della nozione astratta di

algoritmo• Ad ogni stadio tengo conto di pochi

simboli• La prossima mossa dipende solo dai

simboli che sto considerando e dallo stato in cui mi trovo

Non e’ restrittivo assumere che• Scrivo su tanta carta quadrettata quanta

me ne serve (una sola striscia)• Considero solo un carattere alla volta• Mi muovo di un solo quadretto alla volta

Turing’s Worldhttp://www-csli.stanford.edu/hp/Logic-software.html

Macchine di Turing

Introduced by Alan Turing in 1936, Turing machines are one of the key abstractions used in modern computability theory, the study of what computers can and cannot do.

A Turing machine is a particularly simple kind of computer, one whose operations are limited to reading and writing symbols on a tape, or moving along the tape to the left or right.

The tape is marked off into squares, each of which can be filled with at most one symbol. At any given point in its operation, the Turing machine can only read or write on one of these squares, the square located directly below its "read/write" head.

In Turing's World the tape is represented by a narrow window that sits at the bottom of the screen. Here is what the tape looks like

A Turing machine has a finite number of states and is in exactly one of these states at any given time. Associated with these states are instructions telling the machine what action to perform if it is currently scanning a particular symbol, and what state to go into after performing this action. The states of a Turing machine are generally represented by a flow or state diagram, using circles for the states and labelled arcs for the instructions associated with those states.

Here, for example, is a state diagram of a Turing machine with two states. When it is in state 0 looking at an A, this machine will move right one square and return to state 0. When it is in state 0 scanning a B, it will change this symbol to an A and go into state 1.

This machine will run down a string of A's and B's, stopping at the first A it sees after a B.

When you run a Turing machine in Turing's World, the operation of the machine is displayed graphically, both on the tape and in the state diagram window. On the tape, the read/write head moves, making the changes required by the machine you've designed. In the state diagram, the nodes and arcs highlight to show the changing state of the computation.

La codifica

• Una macchina di Turing e’ caratterizzata dall’insieme delle sue istruzioni

• Una macchina ti Turing puo’ essere rappresentata mediante una stringa di caratteri

P 2 : 2 <- QQ 1 : 1 -> P

_|_|_|_|_|_|_|_|_|_|$|Q|1|1|->|P|#|P|2|2|<-|Q|$|_|_|_|_|_|_|_|

Turing: Macchine Universali

[…]

But the most audacious and far-reaching idea he came up with for testing the validity of what he had done was the universal machine.

Think of two natural numbers written on a Turing machine tape […] separated by a blank square. The first number is to be the code number of some Turing machine, and the second is to be an input to that machine:

_|_|_|_|_|_|_|$|…Codifica di M…|$|_|…input per M…|_|_|_|_|_|_|_|_|_|

[…]This would be one single Turing machine that, all by itself, could doanything that any Turing machine could do.

--------------------------------------------------------------------Martin Davis 2000

Model-checkers come Macchine Universali

• Prendo in input una codifica del diagramma degli stati di un sistema (e una formula)

• Simulo il comportamento del mio sistema (per verificare la formula)

• Se il sistema non verifica la formula me ne accorgo (e so anche dire dove il sistema non e’ corretto!)

Model Checking

Model –Checking: I nomi importanti

• Clarke, Emerson e Sistla: inventano la tecnica di base nel 1983

• Bryant: introduce gli Ordered Binary Decision Diagrams (OBDD) nel 1986

• Ken Mc Millan: introduce la versione simbolica usando la codifica di Bryant nel 1989

Copyright 2000 Cadence Design Systems. Permission is granted to reproduce without

modification.

What is f ormal verification?

• Formal means two things:– A mathematical (not English) specifi cation– An exhaustive verifi cation method (not simulation)

• Sometimes “semiformal” is used to mean…– Formal specifi cation, but not verifi cation, or– Nothing f ormal, but using similar algorithms.

Informal simulation methodology...

simulatorsystemvectors

01011...01011...

(observe output)

“Semiformal” simulation methodology...

simulatorsystemvectors

01011...01011...

? properties

Formal verification methodology...

verifiersystem

properties yes/no/?

Copyright 2000 Cadence Design Systems. Permission is granted to reproduce without

modification.

Formal methodsI nf ormal simulation methodology...

simulatorsystemvectors

01011...01011...

(observe output)

“Semiformal” simulation methodology...

simulatorsystemvectors

01011...01011...

? properties

Formal verifi cation methodology...

verifi ersystem

properties yes/ no/ ?

Copyright 2000 Cadence Design Systems. Permission is granted to reproduce without

modification.

Model checking

Verifi cation engine: state space search (even harder!)

Advantage: greater expressiveness(but model must still be fi nite-state)

MC

G(req -> F ack)yes

no/ counterexample:req

ack req

ack

properties:

G(ack1 ack2)

system:

Copyright 2000 Cadence Design Systems. Permission is granted to reproduce without

modification.

Example -- simple pipeline

• Goal: prove equivalence to unpipelined model(modulo delay)

32 registers

+

bypass

32 bits

control

L’esempio precedente: dimensioni

• registri da 32 bit• 8 registri in tutto• 1 sola operazione • 2 pipe register

12010 Stati!

Copyright 2000 Cadence Design Systems. Permission is granted to reproduce without

modification.

Refinement of cache protocol

S/F network

protocol

hostprotocol

host

protocol

host

Distributedcachecoherence

INTF

P P

M IO

to net

• Non-deterministic reference model

• Atomic actions• Single address abstraction• Verifi ed coherence, etc...

IEEEThe IEEE ("eye-triple-E"), The Institute of Electrical and Electronics Engineers, Inc., helps advance global prosperity by promoting the engineering process of creating, developing, integrating, sharing, and applying knowledge about electrical and information technologies and sciences for the benefit of humanity and the profession.

The IEEE publishes more than 30% of the world's literature in electrical engineering and computer science, and IEEE journals and magazines remain the top-cited publications in their respective fields.

IEEE members subscribe at greatly reduced rates.Join the IEEE now!

FUTUREBUS+

IEEE Standard 896.1-1991(IEEE Standard for Futurebus+--Logical

Protocol Specification)Designation: 896.1-1991

Sponsor: Computer/Microprocessors & Microcomputers

Title: IEEE Standard for Futurebus+® — Logical Protocol Specification

Status: Withdrawn Standard. No longer endorsed by the IEEE. Available for purchase as archive document from Global Engineering, Phone: 1-800-854-7179, Fax: 303-397-2740. Outside the U.S. call 303-792-2181. **Sold as ISO/IEC 10857 with 896.1a.

Ken Mc Millan: SMV

•Verifica eseguita con SMV•2300 linee di codice•2 famiglie di errori:

•Scenari inconsistenti ammessi•Deadlocks

x1*x2 + x3*x4 + x5*x6 + x7*x8

-((-(-x3*x2)+-((-((-x2+x1)*(-x6+x4)*(-x10+x8)*(-x14+x12)*(-x18+x16)*(-x22+x20)*(-x26+x24)*(-x30+x28)*(-x34+x32)))*-(-x2+x1)+-(-((-x2+x1)*(-x6+x4)*(-x10+x8)*(-x14+x12)*(-x18+x16)*(-x22+x20)*(-x26+x24)*(-x30+x28)*(-x34+x32)))*(-x2+x1)))*(-(-x7*x6)+-((-((-x2+x1)*(-x6+x4)*(-x10+x8)*(-x14+x12)*(-x18+x16)*(-x22+x20)*(-x26+x24)*(-x30+x28)*(-x34+x32)))*-(-x6+x4)+-(-((-x2+x1)*(-x6+x4)*(-x10+x8)*(-x14+x12)*(-x18+x16)*(-x22+x20)*-x26+x24)*(-x30+x28)*(-x34+x32)))*(-x6+x4)))*(-(-x11*x10)+-((-((-x2+x1)*(-x6+x4)*(-x10+x8)*(-x14+x12)*(-x18+x16)*(-x22+x20)*(-x26+x24)*(-x30+x28)*(-x34+x32)))*-(-x10+x8)+-(-((-x2+x1)*(-x6+x4)*(-x10+x8)*(-x14+x12)*(-x18+x16)*(-x22+x20)*(-x26+x24)*(-x30+x28)*(-x34+x32)))*(-x10+x8)))*(-(-x15*x14)+-((-((-x2+x1)*(-x6+x4)*(-x10+x8)*(-x14+x12)*(-x18+x16)*(-x22+x20)*(-x26+x24)*(-x30+x28)*(-x34+x32)))*-(-x14+x12)+-(-((-x2+x1)*(-x6+x4)*(-x10+x8)*(-x14+x12)*(-x18+x16)*(-x22+x20)*(-x26+x24)*(-x30+x28)*(-x34+x32)))*(-x14+x12)))*(-(-x19*x18)+-((-((-x2+x1)*(-x6+x4)*(-x10+x8)*(-x14+x12)*(-x18+x16)*(-x22+x20)*(-x26+x24)*(-x30+x28)*(-x34+x32)))*-(-x18+x16)+-(-((-x2+x1)*(-x6+x4)*(-x10+x8)*(-x14+x12)*(-x18+x16)*(-x22+x20)*(-x26+x24)*(-x30+x28)*(-x34+x32)))*(-x18+x16)))*(-(-x23*x22)+-((-((-x2+x1)*(-x6+x4)*(-x10+x8)*(-x14+x12)*(-x18+x16)*(-x22+x20)*(-x26+x24)*(-x30+x28)*(-x34+x32)))*-(-x22+x20)+-(-((-x2+x1)*(-x6+x4)*(-x10+x8)*(-x14+x12)*(-x18+x16)*(-x22+x20)*(-x26+x24)*(-x30+x28)*(-x34+x32)))*(-x22+x20)))*(-(-x27*x26)+-((-((-x2+x1)* (-x6+x4)*(-x10+x8)*(-x14+x12)*(-x18+x16)*(-x22+x20)*(-x26+x24)*(-x30+x28)*(-x34+x32)))*-(-x26+x24)+-(-((-x2+x1)* (-x6+x4)*(-x10+x8)*(-x14+x12)*(-x18+x16)*(-x22+x20)*(-x26+x24)*(-x30+x28)*(-x34+x32)))*(-x26+x24)))*(-(-x31*x30)+-((-((-x2+x1)*(-x6+x4)*(-x10+x8)*(-x14+x12)*(-x18+x16)*(-x22+x20)*(-x26+x24)*(-x30+x28)*(-x34+x32)))*-(-x30+x28)+-(-((-x2+x1)*(-x6+x4)*(-x10+x8)*(-x14+x12)*(-x18+x16)*(-x22+x20)*(-x26+x24)*(-x30+x28)*(-x34+x32)))*(-x30+x28)))*(-(-x35*x34)+-(-(-((-x2+x1)*(-x6+x4)*(-x10+x8)*(-x14+x12)*(-x18+x16)*(-x22+x20)*(-x26+x24)*(-x30+x28)*(-x34+x32)))*-(-x34+x32)+-(-((-x2+x1)*(-x6+x4)*(-x10+x8)*(-x14+x12)*(-x18+x16)*(-x22+x20)*(-x26+x24)*(-x30+x28)*(-x34+x32)))*(-x34+x32))))

(x1*x4*x7+x2*-x3*-x10*x13)*-x11 + (x3+x4*-x5*-x12*x15*x13)*x6 + (x5*x14+x6*-x7*-x8*x9)* -x2 + (x7*x8* x9+x8*x9*x1*x2*x3)*x14 + -x12*x16*x17*-x18*x19*x20 + x3*x4*x21*x22*x23*x24*-x25*x26*x27* x28*x29*x30+x1*-x6*x12*-x20*x26*-x30 + x21*-x22*-x23*x24*-x25*x26*x27*-x28 + x16*-x23 + x18*x29 + x23* -x30 + x8*-x16*x17*x23*-x24 + x9*x15*-x21*x27*-x29

Conclusioni

oggi ci sono divisioni di formal methods alla AT&T, IBM, SIEMENS, etc.

si potrebbe dire “niente di nuovo sotto il sole”...

...oppure riconoscere che ci vuole un altro ingrediente: il coraggio (intellettuale) di applicare vecchie idee a nuovi problemi

Martin e Virginia Davis