Presentazione

La Macchina Universale.
Vecchie idee e nuove applicazioni.
Alberto Policriti
Dipartimento di Matematica e Informatica,
Universita’ di Udine.
The Universal Computer
The 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.
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.
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.
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 Turing
http://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 World
http://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
Q 1 : 1 -> P
P 2 : 2 <- Q
• Una macchina ti Turing puo’ essere
rappresentata mediante una stringa di
caratteri
_|_|_|_|_|_|_|_|_|_|$|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
What is formal verification?
• Formal means two things:
– A mathematical (not English) specification
– An exhaustive verification method (not simulation)
• Sometimes “semiformal” is used to mean…
– Formal specification, but not verification, or
– Nothing formal, but using similar algorithms.
Copyright 2000 Cadence Design Systems.
Informal simulation methodology...
system
vectors
01011...
simulator
01011...
(observe output)
“Semiformal” simulation methodology...
system
vectors
01011...
simulator
01011...
?
properties
Formal verification methodology...
system
properties
verifier
yes/no/?
Formal methods
Informal simulation methodology...
system
vectors
01011...
simulator
01011...
(observe output)
“Semiformal” simulation methodology...
system
vectors
01011...
simulator
01011...
?
properties
Formal verification methodology...
system
properties
verifier
Copyright 2000 Cadence Design Systems.
yes/no/?
Model checking
properties:
G(req -> F ack)
yes
G(ack1ack2)
MC
system:
req
no/counterexample:
req
ack
ack
Verification engine: state space search (even harder!)
Advantage: greater expressiveness
(but model must still be finite-state)
Copyright 2000 Cadence Design Systems.
Example -- simple pipeline
32 bits
32 registers
control
+
bypass
• Goal: prove equivalence to unpipelined model
(modulo delay)
Copyright 2000 Cadence Design Systems.
L’esempio precedente:
dimensioni
•
•
•
•
registri da 32 bit
8 registri in tutto
1 sola operazione
2 pipe register
10
120
Stati!
Refinement of cache protocol
P
M
P
INTF
to net
host
Distributed
cache
coherence
protocol
IO
• Non-deterministic reference
model
• Atomic actions
• Single address abstraction
• Verified coherence, etc...
host
protocol
S/F network
Copyright 2000 Cadence Design Systems.
host
protocol
IEEE
The 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