On a simple example of non-deterministic programming, we demonstrate that the delimited control operator `shift`

is akin to a user-level `fork`

.

- The puzzle
- Solving the puzzle using non-determinism
- Implementing
`SimpleNonDet`

via`fork(2)`

- Implementing
`SimpleNonDet`

via`shift`

- puzzle.ml [6K]

The complete commented OCaml code solving the puzzle, with the two implementations of the simple library of non-determinism - Delimited Control in OCaml, Abstractly and Concretely: System description

The puzzle served as an introduction to the delimcc library in the FLOPS 2010 talk.

- Our example is the following puzzle, which I received from a friend of mine back in 1998.
- ``U2 has a concert that starts in 17 minutes and they must all cross a bridge to get there. All four men begin on the same side of the bridge. It is night. There is one flashlight. A maximum of two people can cross at one time. Any party who crosses, either 1 or 2 people, must have the flashlight with them. The flashlight must be walked back and forth, it cannot be thrown, etc.. Each band member walks at a different speed. A pair must walk together at the rate of the slower man's pace:''
Bono: 1 minute to cross Edge: 2 minutes to cross Adam: 5 minutes to cross Larry: 10 minutes to cross

Allegedly, this was a question for potential Microsoft employees. An answer was expected within 5 minutes.

- ``U2 has a concert that starts in 17 minutes and they must all cross a bridge to get there. All four men begin on the same side of the bridge. It is night. There is one flashlight. A maximum of two people can cross at one time. Any party who crosses, either 1 or 2 people, must have the flashlight with them. The flashlight must be walked back and forth, it cannot be thrown, etc.. Each band member walks at a different speed. A pair must walk together at the rate of the slower man's pace:''

- The puzzles like ours are elegantly solved with non-determinism. Here is the gist of a sample solution:
type u2 = Bono | Edge | Adam | Larry type side = u2 list let rec loop trace forward time_left = function | ([], _) when forward -> (* nobody is on the original side *) print_trace (List.rev trace) | (_, []) when not forward -> (* nobody is on the original side *) print_trace (List.rev trace) | (side_from, side_to) -> let party = select_party side_from in let elapsed = elapsed_time party in let _ = if elapsed > time_left then fail () in let side_from' = without party side_from in let side_to' = side_to @ party in loop ((party,forward)::trace) (not forward) (time_left - elapsed) (side_to',side_from')

The function`loop`

recites the statement of the problem, in a formal way. The code states that groups of people walk across the bridge in alternating directions; the code keeps track of the elapsed time and of the crossing log, which is printed when nobody remains on the original side of the bridge. Most of the functions are trivial:`elapsed_time`

computes the crossing time for a party of people;`without`

is list ``subtraction,'' sort of the opposite for the list append, operator`@`

. Two interesting functions are`select_party`

to non-deterministically choose one or two people to cross the bridge, and`fail`

to report that we have made what turns out bad choices (that is, we exceeded the time allowance).These two functions are easy to implement if we have a library with the following simple interface. The function

`choose`

non-deterministically selects an element from a given list, and the function`run`

executes the non-deterministic computation. We assume that the computation would print out its result when it finishes. Therefore, its return type, and the return type of`run`

are`unit`

.module type SimpleNonDet = sig val choose : 'a list -> 'a val run : (unit -> unit) -> unit end

We can implement the needed non-deterministic functions as:let select_party side = let p1 = choose side in let p2 = choose side in match compare p1 p2 with | 0 -> [p1] | n when n < 0 -> [p1;p2] | _ -> fail () let fail () = choose []

We run the computation as follows, obtaining the print-out of two solutions.run (fun () -> loop [] true 17 ([Bono;Edge;Adam;Larry],[]));;

`SimpleNonDet`

via `fork(2)`

- We demonstrate two implementations of the SimpleNonDet interface. The first one relies on the operating system call
`fork`

let rec choose = function | [] -> exit 666 | [x] -> x | (h::t) -> let pid = fork () in if pid = 0 then h else wait (); choose t let run m = match fork () with | 0 -> m (); printf "Solution found"; exit 0 | _ -> try while true do waitpid [] 0 done with ...

to split the computation at the choice point, so we can try all the choices, perhaps in parallel, and hope one of them eventually succeeds. It is mildly fascinating to observe the execution using top, watching the processes multiply and wither. The function`run`

too uses fork, to split the computation into a process that does all the work, and the supervisor. The supervisor immediately goes to sleep, waiting for all the workers to finish so it can report a success or an exception. Since Unix threads are quite heavy-weight, the implementation is slow. We need green processes.

`SimpleNonDet`

via `shift`

- The library delimcc gives us such green processes for OCaml. We implement the same
`SimpleNonDet`

interface using the delimited control operators`shift`

and`push_prompt`

.open Delimcc let p = new_prompt () let choose xs = shift p (fun k -> List.iter k xs) let run m = push_prompt p m

The function`shift`

is like`fork`

; however, rather than returning a`pid`

to the parent process,`shift`

returns to the parent the representation`k`

of the child process, as a function. In the code above, the parent process is the body of`shift`

, namely`List.iter k xs`

. The child process -- the code where shift appears -- is suspended. When the parent applies`k`

to a value, the child process is resumed with that value. The function`push_prompt`

too splits the computation, creating the worker that executes`m`

, and the supervisor that waits, handles failures and reports the result. The prompt`p`

is akin to a communication channel, which the child process uses to tell the supervisor of its final result or exception.

oleg-at-okmij.org

Your comments, problem reports, questions are very welcome!

Converted from HSXML by HSXML->HTML