previous  next  up  top

shift as a green fork (2)

 

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

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
For example: if Adam and Larry walk across first, 10 minutes have elapsed when they get to the other side of the bridge. If Adam then returns with the flashlight, a total of 15 minutes have passed. There is no way Adam, Bono and Edge could make it across the bridge in the remaining 2 minutes.

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

 

Solving the puzzle using non-determinism

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],[]));;

 

Implementing 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.

 

Implementing 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.

Last updated May 7, 2010

This site's top page is http://okmij.org/ftp/

oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!

Converted from HSXML by HSXML->HTML