diff --git a/hpaxos/hpaxos-message.sml b/hpaxos/hpaxos-message.sml index 1e10e0a..bff776d 100644 --- a/hpaxos/hpaxos-message.sml +++ b/hpaxos/hpaxos-message.sml @@ -1,65 +1,110 @@ -(* HPaxos Message *) +structure HPaxosMessage (*: HPAXOS_MESSAGE*) = +struct + infix |> + fun x |> f = f x -signature HPAXOS_VALUE = -sig - type t - val default : t (* default value *) - val eq : t * t -> bool (* equality *) -end + type hash = word -signature HPAXOS_BALLOT = -sig - type t - val zero : t (* the smallest ballot *) - val eq : t * t -> bool - val compare : t * t -> order -end - -signature HPAXOS_MESSAGE = -sig - type t - datatype typ = OneA - | OneB - | TwoA + structure Learner = Learner + type learner = Learner.t - structure Value : HPAXOS_VALUE + structure Value = HPaxosValue type value = Value.t - structure Ballot : HPAXOS_BALLOT + structure Ballot = HPaxosBallot type ballot = Ballot.t - structure Learner : LEARNER - type learner = Learner.t - - structure Acceptor : ACCEPTOR + structure Acceptor = HPaxosAcceptor type acceptor = Acceptor.t - val hash : t -> word - val eq : t * t -> bool - - val typ : t -> typ - - val is_one_a : t -> bool - val is_one_b : t -> bool - val is_two_a : t -> bool + datatype msg = + OneA of ( + ballot * (* ballot *) + hash (* message hash *) + ) + | OneB of ( + acceptor * (* sender *) + msg list * (* references *) + msg option * (* previous message *) + hash (* message hash *) + ) + | TwoA of ( + acceptor * (* sender *) + msg list * (* references *) + msg option * (* previous message *) + learner list * (* list of learners *) + hash (* message hash *) + ) + + type t = msg + + fun hash (OneA (_, h) | OneB (_, _, _, h) | TwoA (_, _, _, _, h)) = h + + fun compute_hash (OneA (bal, _)) = + Ballot.hash bal + | compute_hash (OneB (_, refs, prev, _)) = + let + val refs_hash = List.map hash refs + val prev_hash = map_or prev [] (fn p => [hash p]) + val hashes = [prev_hash, refs_hash] |> List.concat + in + Hashing.hash hashes + end + | compute_hash (TwoA (_, refs, prev, lrs, _)) = + let + val refs_hash = List.map hash refs + val prev_hash = map_or prev [] (fn p => [hash p]) + val lrs_hash = List.map Learner.hash lrs + val hashes = [prev_hash, refs_hash, lrs_hash] |> List.concat + in + Hashing.hash hashes + end - val mk_one_b : t option * t list -> t - val mk_two_a : t option * t list * learner -> t + (* TODO check if equality is used *) + fun eq (OneA (_, h1), OneA (_, h2)) = h1 = h2 + | eq (OneB (_, _, _, h1), OneB (_, _, _, h2)) = h1 = h2 + | eq (TwoA (_, _, _, _, h1), TwoA (_, _, _, _, h2)) = h1 = h2 + | eq (_, _) = false - (* if the message is 2a, return its learner instance; otherwise, return NONE *) - val learner : t -> learner option + (* fun typ (Msg (t, _, _, _, _)) = t *) - (* returns message sender *) - val sender : t -> acceptor + fun is_one_a (OneA _) = true + | is_one_a _ = false - (* if the message is 1a, return its ballot and value; otherwise, return NONE *) - val get_bal_val : t -> (ballot * value) option + fun is_one_b (OneB _) = true + | is_one_b _ = false - (* returns a previous message of the sender *) - val get_prev : t -> t option + fun is_two_a (TwoA _) = true + | is_two_a _ = false - (* returns a list of direct references *) - val get_refs : t -> t list + (* TODO this should be raw? *) + fun mk_one_b (sender, prev_msg, recent_msgs) = + let val hash = Word.fromInt 42 in + OneB (sender, recent_msgs, prev_msg, hash) + end + + (* TODO this should be raw? *) + fun mk_two_a (sender, prev_msg, recent_msgs, learners) = + let val hash = Word.fromInt 42 in + TwoA (sender, recent_msgs, prev_msg, learners, hash) + end + + fun learners (TwoA (_, _, _, ls, _)) = ls + | learners _ = [] + + fun sender (OneB (sender, _, _, _)) = sender + | sender (TwoA (sender, _, _, _, _)) = sender + | sender _ = raise Fail "sender not defined" + + fun get_bal_val (OneA (b, _)) = + let val v = Ballot.value b in SOME (b, v) end + | get_bal_val _ = NONE + + fun get_prev (OneA _) = NONE + | get_prev (OneB (_, _ , prev, _) | TwoA (_, _ , prev, _, _)) = prev + + fun get_refs (OneA _) = [] + | get_refs (OneB (_, refs , _, _) | TwoA (_, refs , _, _, _)) = refs end functor MessageOrdKey (Msg : HPAXOS_MESSAGE) : ORD_KEY = @@ -72,6 +117,9 @@ functor MessageUtil (Msg : HPAXOS_MESSAGE) = struct structure MsgSet : ORD_SET = RedBlackSetFn (MessageOrdKey (Msg)) + type msg = Msg.t + type ballot = Msg.Ballot.t + (* fun does_reference_1a m : bool = *) (* isSome (List.find Msg.is_one_a (Msg.get_refs m)) *) @@ -101,8 +149,8 @@ struct (* checks if m2 is in transitive closure of prev for m1 *) structure PrevTran :> sig - val is_prev_reachable : Msg.t * Msg.t -> bool - val is_prev_reachable' : (Msg.t -> Msg.Ballot.t) -> Msg.t * Msg.t -> bool + val is_prev_reachable : msg * msg -> bool + val is_prev_reachable' : (msg -> ballot) -> msg * msg -> bool end = struct fun is_prev_reachable_aux cont (m1, m2) = @@ -129,7 +177,7 @@ struct end (* PrevTran *) (* compute transitive references of the message *) - fun tran pred cont m = + fun tran (pred : msg -> bool) (cont : msg -> bool) (m : msg) = let fun loop accu visited [] = accu | loop accu visited (x :: tl) =