On a simple example of non-deterministic programming, we demonstrate that the delimited control operator
shift is akin to a user-level
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.
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
looprecites 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_timecomputes the crossing time for a party of people;
withoutis list ``subtraction,'' sort of the opposite for the list append, operator
@. Two interesting functions are
select_partyto non-deterministically choose one or two people to cross the bridge, and
failto 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
module type SimpleNonDet = sig val choose : 'a list -> 'a val run : (unit -> unit) -> unit endWe 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],));;
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
runtoo 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.
SimpleNonDetinterface using the delimited control operators
open Delimcc let p = new_prompt () let choose xs = shift p (fun k -> List.iter k xs) let run m = push_prompt p mThe function
fork; however, rather than returning a
pidto the parent process,
shiftreturns to the parent the representation
kof the child process, as a function. In the code above, the parent process is the body of
List.iter k xs. The child process -- the code where shift appears -- is suspended. When the parent applies
kto a value, the child process is resumed with that value. The function
push_prompttoo splits the computation, creating the worker that executes
m, and the supervisor that waits, handles failures and reports the result. The prompt
pis akin to a communication channel, which the child process uses to tell the supervisor of its final result or exception.
oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML