Dijkstra 1965 (Go)

945526.945527.pdf

README.md

Dijkstra 1965

Implementation of "Solution of a Problem in Concurrent Programming Control" (1965) by Dijkstra in Go.

• Paper: http://rust-class.org/static/classes/class19/dijkstra.pdf
• Java Implementation: https://gist.github.com/glts/4494246b894e6424d0c3

dijkstra65.go

// Solution of a Problem in Concurrent Program Control
//
// Dijkstra, 1965: http://rust-class.org/static/classes/class19/dijkstra.pdf
// https://i.imgur.com/weHFuip.png
//
// Notes:
//
// * if b[i] is true, then the program is not "looping", e.g. not waiting to enter a critical section
// * if b[i] is false (Li0), the program entered "looping" stage, before the critical section
//
// k looks like a "selector", the "if" statement in Li1 like a two-stage "check"
//
//     First we want k and i be the same; which only happens, if current
//     program k is not waiting (i.e. b[k] is true).
//
//     If the program at k is not waiting, we can jump to the next branch (Li4).
//
//     Here, we want all other programs not in the critical section; also
//     setting c[i] to false to indicate, that we want to run.
//
package main

import (
	"bytes"
	"flag"
	"fmt"
	"io"
	"math/rand"
	"time"
)

const (
	Enter = "\u001b[32mE\u001b[0m"
	Exit  = "\u001b[31mX\u001b[0m"
	False = "\u001b[34mF\u001b[0m"
	True  = "\u001b[37mT\u001b[0m"
)

var (
	N    = flag.Int("n", 3, "number of processes")
	T    = flag.Duration("t", 1000*time.Millisecond, "exit simulation after t (e.g. 1s, 100ms, ...)")
	Cdur = flag.Duration("C", 10*time.Millisecond, "critical section duration")
	Rdur = flag.Duration("R", 100*time.Millisecond, "remainder duration")
)

func main() {
	flag.Parse()
	// The integer k will satisfy 1 <= k <= N, b[i] and c[i] will only be set
	// by the ith computer; they will be inspected by others. [...] all
	// boolean arrays mentioned set to true. The starting value of k is
	// immaterial.
	var (
		k int = 0
		b     = make([]bool, *N)
		c     = make([]bool, *N)
	)
	setTrue(b)
	setTrue(c)

	// The program for the ith computer [...]
	computer := func(i int) {
		fmt.Printf("[%d] R .. k=%v, b=%v, c=%v\n", i, k, Btoa(b), Btoa(c))
	Li0:
		fmt.Printf("[%d] Li0  k=%v, b=%v, c=%v\n", i, k, Btoa(b), Btoa(c))
		b[i] = false
	Li1:
		if k != i {
			c[i] = true
			// Li3
			if b[k] {
				k = i
			}
			goto Li1
		} else {
			// Li4
			c[i] = false
			for j := 0; j < *N; j++ {
				if j != i && !c[j] {
					goto Li1
				}
			}
		}
		// Critical section, only at most one "computer" will be in this section at any time.
		fmt.Printf("[%d] %s >> k=%v, b=%v, c=%v\n", i, Enter, k, Btoa(b), Btoa(c))
		time.Sleep(*Cdur)
		fmt.Printf("[%d] %s << k=%v, b=%v, c=%v\n", i, Exit, k, Btoa(b), Btoa(c))
		// Critical section ends.

		c[i] = true
		b[i] = true

		fmt.Printf("[%d] Rem  k=%v, b=%v, c=%v\n", i, k, Btoa(b), Btoa(c))
		time.Sleep(time.Duration(rand.Int63n(Rdur.Milliseconds())) * time.Millisecond)
		goto Li0
	}
	for i := 0; i < *N; i++ {
		go computer(i)
	}
	time.Sleep(*T)
	fmt.Println("[X] timeout")
}

func setTrue(b []bool) {
	for i := 0; i < len(b); i++ {
		b[i] = true
	}
}

func Btoa(b []bool) string {
	var buf bytes.Buffer
	for _, v := range b {
		if v {
			io.WriteString(&buf, True)
		} else {
			io.WriteString(&buf, False)
		}
	}
	return buf.String()
}

// Appendix A: The Proof
//
// We start b y observing that the solution is safe in the
// sense that no two computers can be in their critical section
// simultaneously. For the only way to enter its critical
// section is the performance of the compound statement
// Li4 without jmnping back to Lil, i.e., finding all other
// c's t r u e after having set its own e to false.
// The second part of the proof must show that no infinite
// "After you"-"After you"-blocking can occur; i.e., when
// none of the computers is in its critical section, of the
// computers looping (i.e., jumping back to Lil) at least
// one--and therefore exactly one--will be allowed to enter
// its critical section in due time.
// If the kth computer is not among the looping ones,
// bik] will be t r u e and the looping ones will all find k # i.
// As a result one or mnore of them will find in Li3 the Boolean
// b[k] t r u e and therefore one or more will decide to assign
// "k : = i". After the first assignment "k : = i", b[k] becomes false and no new computers can decide again to
// assign a new value to k. When all decided assignments to
// k have been performed,/c will point to one of the looping
// computers and will not change its value for the time being,
// i.e., until b[k] becomes t r u e , viz., until the kth computer
// has completed its critical section. As soon as the value of
// ]c does not change any more, the kth computer will wait
// (via the compound statement Li4) until all other c's are
// t r u e , but this situation will certainly arise, if not already
// present, because all other looping ones are forced to set
// their e t r u e , as they will find k # i. And this, the author
// believes, completes the proof.
//
// Appendix B: Race
// ==================
// WARNING: DATA RACE
// Write at 0x00c0000bc051 by goroutine 8:
//   main.main.func1()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:65 +0xf8e
//
// Previous read at 0x00c0000bc051 by goroutine 7:
//   main.Btoa()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:111 +0xb5
//   main.main.func1()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:84 +0x536
//
// Goroutine 8 (running) created at:
//   main.main()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:97 +0x504
//
// Goroutine 7 (running) created at:
//   main.main()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:97 +0x504
// ==================
// ==================
// WARNING: DATA RACE
// Write at 0x00c0000bc054 by goroutine 8:
//   main.main.func1()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:68 +0x364
//
// Previous read at 0x00c0000bc054 by goroutine 9:
//   main.Btoa()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:111 +0xb5
//   main.main.func1()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:64 +0xdb3
//
// Goroutine 8 (running) created at:
//   main.main()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:97 +0x504
//
// Goroutine 9 (running) created at:
//   main.main()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:97 +0x504
// ==================
// ==================
// WARNING: DATA RACE
// Read at 0x00c0000bc055 by goroutine 7:
//   main.Btoa()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:111 +0xb5
//   main.main.func1()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:86 +0x7fc
//
// Previous write at 0x00c0000bc055 by goroutine 9:
//   main.main.func1()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:68 +0x364
//
// Goroutine 7 (running) created at:
//   main.main()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:97 +0x504
//
// Goroutine 9 (running) created at:
//   main.main()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:97 +0x504
// ==================
// ==================
// WARNING: DATA RACE
// Write at 0x00c0000bc050 by goroutine 7:
//   main.main.func1()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:90 +0xa5d
//
// Previous read at 0x00c0000bc050 by goroutine 9:
//   main.main.func1()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:70 +0x3ea
//
// Goroutine 7 (running) created at:
//   main.main()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:97 +0x504
//
// Goroutine 9 (running) created at:
//   main.main()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:97 +0x504
// ==================
// ==================
// WARNING: DATA RACE
// Write at 0x00c0000bc048 by goroutine 8:
//   main.main.func1()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:71 +0x418
//
// Previous read at 0x00c0000bc048 by goroutine 7:
//   main.main.func1()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:86 +0x844
//
// Goroutine 8 (running) created at:
//   main.main()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:97 +0x504
//
// Goroutine 7 (running) created at:
//   main.main()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:97 +0x504
// ==================
// ==================
// WARNING: DATA RACE
// Write at 0x00c0000bc053 by goroutine 7:
//   main.main.func1()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:68 +0x364
//
// Previous read at 0x00c0000bc053 by goroutine 8:
//   main.main.func1()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:78 +0x4dd
//
// Goroutine 7 (running) created at:
//   main.main()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:97 +0x504
//
// Goroutine 8 (running) created at:
//   main.main()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:97 +0x504
// ==================
// ==================
// WARNING: DATA RACE
// Read at 0x00c0000bc052 by goroutine 7:
//   main.Btoa()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:111 +0xb5
//   main.main.func1()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:64 +0xd64
//
// Previous write at 0x00c0000bc052 by goroutine 9:
//   main.main.func1()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:90 +0xa5d
//
// Goroutine 7 (running) created at:
//   main.main()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:97 +0x504
//
// Goroutine 9 (running) created at:
//   main.main()
//       /home/tir/code/miku/18d13ab0c7de09120a26f8ebe153ad27/dijkstra65.go:97 +0x504
// ==================
// Found 7 data race(s)
// exit status 66

dijkstra65.pdf

minimal.go

// Solution of a Problem in Concurrent Program Control, http://rust-class.org/static/classes/class19/dijkstra.pdf
package main

import (
	"flag"
	"time"
)

var (
	N    = flag.Int("n", 3, "number of processes")
	T    = flag.Duration("t", 1000*time.Millisecond, "exit simulation after t (e.g. 1s, 100ms, ...)")
	Cdur = flag.Duration("C", 10*time.Millisecond, "critical section duration")
)

func main() {
	flag.Parse()
	var (
		k        int = 0
		b            = boolSlice(*N, true)
		c            = boolSlice(*N, true)
		computer     = func(i int) {
		Li0:
			b[i] = false
		Li1:
			if k != i {
				c[i] = true
				if b[k] {
					k = i
				}
				goto Li1
			} else {
				c[i] = false
				for j := 0; j < *N; j++ {
					if j != i && !c[j] {
						goto Li1
					}
				}
			}
			time.Sleep(*Cdur) // simulate critical section
			c[i] = true
			b[i] = true
			goto Li0
		}
	)
	for i := 0; i < *N; i++ {
		go computer(i)
	}
	time.Sleep(*T)
}

func boolSlice(n int, iv bool) []bool {
	b := make([]bool, n)
	for i := 0; i < len(b); i++ {
		b[i] = iv
	}
	return b
}

sketch.go

// Attempts at a solution to Dijkstra's 1965 concurrency puzzle.
//
// * N computers, cyclic program
// * each program has one critical section
// * only one critical section is allowed to run
// * computer may communicate by reading and writing to memory (one read and one write is atomic)
//
// Idea
//
// If we have N processes (P1, P2, ..., PN), we require N+1 memory cells.
// P1 wants to enter critical section. It sets M1. P1 checks whether any other
// process cell is set. If so, then it unset M1, sleeps a bit a will reattempt
// then.
//
// If after setting M1, all other cells remain zero, P1 sets M0 and enter
// critical section. Upon leaving, if clears M0 and M1.
package main

import (
	"flag"
	"log"
	"math/rand"
	"time"
)

type Memory struct {
	words []int
}

func New(size int) *Memory {
	return &Memory{words: make([]int, size)}
}

// Set a flag at a position.
func (m *Memory) Set(i int) {
	m.words[i] = 1
}

// Unset clear memory at position.
func (m *Memory) Unset(i int) {
	m.words[i] = 0
}

// IsSet returns true, if memory cell is set.
func (m *Memory) IsSet(i int) bool {
	return m.words[i] == 1
}

// IsZero returns true, if all cells are zero.
func (m *Memory) IsZero() bool {
	for _, b := range m.words {
		if b != 0 {
			return false
		}
	}
	return true
}

// IsZeroExcept returns true, if all positions of memory except position x are zero.
func (m *Memory) IsZeroExcept(x int) bool {
	for i, w := range m.words {
		if i == x {
			continue
		}
		if w != 0 {
			return false
		}
	}
	return true
}

// Lock attempts signal that a process `i` wants to enter its critical section.
// Returns true, if it succeeded.
func (m *Memory) Lock(i int) {
	var attempts = 1
	for {
		if m.IsSet(0) {
			time.Sleep(time.Duration(attempts) * time.Millisecond)
			attempts++
			continue
		}
		m.Set(i)
		if m.IsZeroExcept(i) {
			m.Set(0) // lock acquired
			break
		}
		m.Unset(i)
	}
}

func (m *Memory) Unlock(i int) {
	m.Unset(0)
	m.Unset(i)
}

type Process struct {
	PID     int
	M       *Memory
	counter map[int]int
}

func (p *Process) Run() {
	log.Printf("[%d] started", p.PID)
	var (
		started time.Time
		elapsed time.Duration
	)
	for {
		time.Sleep(time.Duration(rand.Intn(100)) * time.Millisecond)
		started = time.Now()
		p.M.Lock(p.PID)
		elapsed = time.Since(started)
		log.Printf("[%d] entered [%v]", p.PID, elapsed)
		p.counter[p.PID]++
		time.Sleep(time.Duration(rand.Intn(20)) * time.Millisecond)
		p.M.Unlock(p.PID)
		log.Printf("[%d] exit", p.PID)
	}
}

var (
	N    = flag.Int("n", 2, "number of processes")
	T    = flag.Duration("t", 500*time.Millisecond, "exit simulation after t seconds")
	seed = flag.Int64("S", time.Now().UTC().UnixNano(), "seed")
)

func main() {
	flag.Parse()
	rand.Seed(*seed)
	var (
		m       = New(*N + 1)
		counter = make(map[int]int)
	)
	log.Printf("initialized memory: %v", m)
	for i := 1; i <= *N; i++ {
		counter[i] = 0
		process := &Process{
			PID:     i,
			M:       m,
			counter: counter,
		}
		go process.Run()
	}
	time.Sleep(*T)
	log.Println("[X] timeout")
	for k, v := range counter {
		log.Printf("%d => %d", k, v)
	}
}

// 2021/06/05 01:56:18 initialized memory: &{[0 0 0 0 0 0 0 0 0 0]}
// 2021/06/05 01:56:18 [9] started
// 2021/06/05 01:56:18 [9] entered [374ns]
// 2021/06/05 01:56:18 [1] started
// 2021/06/05 01:56:18 [6] started
// 2021/06/05 01:56:18 [7] started
// 2021/06/05 01:56:18 [8] started
// 2021/06/05 01:56:18 [3] started
// 2021/06/05 01:56:18 [2] started
// 2021/06/05 01:56:18 [4] started
// 2021/06/05 01:56:18 [5] started
// 2021/06/05 01:56:18 [9] exit
// 2021/06/05 01:56:18 [3] entered [16.820926ms]
// 2021/06/05 01:56:18 [3] exit
// 2021/06/05 01:56:18 [5] entered [24.362396ms]
// 2021/06/05 01:56:18 [5] exit
// 2021/06/05 01:56:18 [9] entered [2.15594ms]
// 2021/06/05 01:56:18 [9] exit
// 2021/06/05 01:56:18 [8] entered [10.776265ms]
// 2021/06/05 01:56:18 [8] exit
// 2021/06/05 01:56:18 [3] entered [631ns]
// 2021/06/05 01:56:18 [3] exit
// 2021/06/05 01:56:18 [2] entered [69.099468ms]
// 2021/06/05 01:56:18 [2] exit
// 2021/06/05 01:56:18 [6] entered [15.465933ms]
// 2021/06/05 01:56:18 [6] exit
// 2021/06/05 01:56:18 [4] entered [18.820081ms]
// 2021/06/05 01:56:18 [4] exit
// 2021/06/05 01:56:18 [1] entered [40.404119ms]
// 2021/06/05 01:56:18 [1] exit
// 2021/06/05 01:56:18 [8] entered [498ns]
// 2021/06/05 01:56:18 [8] exit
// 2021/06/05 01:56:18 [4] entered [19.501583ms]
// 2021/06/05 01:56:18 [4] exit
// 2021/06/05 01:56:18 [5] entered [62.11501ms]
// 2021/06/05 01:56:18 [5] exit
// 2021/06/05 01:56:18 [9] entered [13.888874ms]
// 2021/06/05 01:56:18 [9] exit
// 2021/06/05 01:56:18 [2] entered [62.859946ms]
// 2021/06/05 01:56:18 [2] exit
// 2021/06/05 01:56:18 [6] entered [79.3289ms]
// 2021/06/05 01:56:18 [X] timeout