Sir Charles Anthony Richard Hoare or just Dad Quicksort, NULL and Problems of Dining Philosophers

A knight in education and computer science, a peasant in whose honor logic was named, the first to admit one billion dollars of his mistake, the developer of qsort, celebrates his 82nd birthday today, January 11th. (Surely with Whip .)

Quicksort

After talking with Kolmogorov over a tea jar at Moscow State University in 1960, Hoar developed one of the fastest known universal algorithms for sorting arrays: on average, O (n \ log n) exchanges when ordering n elements. Read more on wikipedia .

If someone read it, then here is the explanation of the dance:

')

Logic hoare

A formal system with a set of logical rules designed to prove the correctness of computer programs. It was proposed in 1969 by English scientist in the field of computer science and mathematical logic Hoar, later developed by Hoar himself and other researchers. The initial idea was proposed in the work of Floyd, who published a similar system as applied to flowcharts. ( Read more on wikipedia. )

Interacting sequential processes (Eng. Communicating sequential processes, CSP )

This is a transputer.

Formal language for describing interaction models in parallel systems. It refers to mathematical theories of parallelism, known as calculus of processes (or process algebra), based on the transmission of messages through channels. Influenced the development of the language Ockham, Limbo, Go.

The CSP theory was first described in an article by Charles E. Hoare in 1978. This initial version was unsuccessful because it did not represent unlimited indeterminism. Subsequently, under the influence of ideas borrowed from the model of the actors of Karl Hewitt, the theory was significantly changed. (In modern CSP Hoare from 1985, unlimited indeterminism is used). C since significantly developed. In practice, CSP was used as a tool for formal specification of systems with parallelism (concurrency), such as, for example, a T9000 transputer or a secure e-commerce system. The theory of CSP is still the subject of active research in terms of expanding practical applicability, in particular, increasing the size of the analyzed systems. (Read more on wikipedia .)

The problem of dining philosophers

The problem was formulated in 1965 by Edsger Dijkstra as an examination exercise for students. As an example, was taken competing access to the tape drive. Soon the problem was formulated by Richard Hoar as it is known today.

Five silent philosophers sit around a round table, each philosopher has a plate of spaghetti. The forks lie on the table between each pair of the closest philosophers.

Every philosopher can either eat or meditate. Eating is not limited by the amount of spaghetti remaining - an infinite supply is implied. However, a philosopher can only eat when he holds two forks - taken from the right and left (an alternative formulation of the problem implies bowls of rice and chopsticks instead of plates with spaghetti and forks).

Each philosopher can take the nearest plug (if it is available), or put it - if he is already holding it. Taking each fork and returning it to the table are separate actions that must be performed one after another.

The essence of the problem is to develop a model of behavior (parallel algorithm), in which none of the philosophers will starve, that is, will always alternate food intake and reflection. (Read more on wikipedia .)

Billion error

In 2009, at the QCon conference, Hoar apologized:

“I call it my billion-dollar mistake. Reference: 1965. At that time, it was the first time that it was designed. It was absolutely safe for the compiler. But I couldn’t have been able to implement it . This has led to innumerable errors, health problems, and system crashes. In recent years, there have been a number of risk analyzers that have been used. More recent programming languages ​​like Spec # have declarations for non-null references. This is the solution, which I rejected in 1965. "

Proof video here .

Video lecture "Could computers understand their own programs"

Happy Birthday!