WIP HPaxos 2.0

gen-server-impl.sig

@@ -0,0 +1,9 @@
+signature GEN_SERVER_IMPL =
+sig
+    type param
+    type state
+    type msg
+
+    val init : param -> state
+    val handle_msg : state * msg -> state * msg option
+end

hashing.sml

@@ -0,0 +1,10 @@
+structure Hashing = struct
+    infix |>
+    fun x |> f = f x
+
+    fun hash words =
+        words
+        |> List.map Word.toString
+        |> String.concat
+        |> FNVHash.hashString
+end

hpaxos/hpaxos-acceptor.sig

@@ -0,0 +1,7 @@
+signature ACCEPTOR =
+sig
+    type t
+
+    val pubkey : t -> word
+    val eq : t * t -> bool
+end

hpaxos-acceptor.sml → hpaxos/hpaxos-acceptor.sml

@@ -1,8 +1,9 @@
-signature ACCEPTOR =
-sig
-    type t
-    val pubkey : t -> word
-    val eq : t * t -> bool
+structure HPaxosAcceptor =
+struct
+    type t = word
+
+    fun pubkey a = a
+    val eq : t * t -> bool = (op =)
 end
 
 functor AcceptorOrdKey (A : ACCEPTOR) : ORD_KEY =

hpaxos/hpaxos-ballot.sig

@@ -0,0 +1,13 @@
+signature HPAXOS_BALLOT =
+sig
+    type t
+    type value
+
+    val default : t
+
+    val eq : t * t -> bool
+    val compare : t * t -> order
+    val hash : t -> word
+
+    val value : t -> value
+end

hpaxos/hpaxos-ballot.sml

@@ -0,0 +1,18 @@
+structure HPaxosBallot : HPAXOS_BALLOT =
+struct
+    type t = word
+
+    structure Value = HPaxosValue
+    type value = Value.t
+
+    val default = Word.fromInt 0
+
+    val eq : t * t -> bool = (op =)
+    val compare = Word.compare
+
+    (* TODO *)
+    fun hash b = b
+
+    (* TODO *)
+    fun value b = Value.default
+end

hpaxos/hpaxos-message.sig

@@ -0,0 +1,35 @@
+signature HPAXOS_MESSAGE =
+sig
+    type t
+
+    structure Value : HPAXOS_VALUE
+    type value = Value.t
+
+    structure Ballot : HPAXOS_BALLOT
+    type ballot = Ballot.t
+
+    structure Learner : LEARNER
+    type learner = Learner.t
+
+    structure Acceptor : ACCEPTOR
+    type acceptor = Acceptor.t
+
+    val hash : t -> word
+    val eq : t * t -> bool
+
+    val is_proposal : t -> bool
+
+    val mk_non_proposal : t option * t list -> t
+
+    (* returns message sender *)
+    val sender : t -> acceptor
+
+    (* if the message is a proposal, return its ballot and value; otherwise, return NONE *)
+    val get_bal_val : t -> (ballot * value) option
+
+    (* returns a previous message of the sender *)
+    val get_prev : t -> t option
+
+    (* returns a list of direct references *)
+    val get_refs : t -> t list
+end

hpaxos-message.sml → hpaxos/hpaxos-message.sml

@@ -1,65 +1,76 @@
-(* HPaxos Message *)
-
-signature HPAXOS_VALUE =
-sig
-    type t
-    val default : t (* default value *)
-    val eq : t * t -> bool (* equality *)
-end
+structure HPaxosMessage (*: HPAXOS_MESSAGE*) =
+struct
+    infix |>
+    fun x |> f = f x
 
-signature HPAXOS_BALLOT =
-sig
-    type t
-    val zero : t (* the smallest ballot *)
-    val eq : t * t -> bool
-    val compare : t * t -> order
-end
+    type hash = word
 
-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
-
-    val mk_one_b : t option * t list -> t
-    val mk_two_a : t option * t list * learner -> t
-
-    (* if the message is 2a, return its learner instance; otherwise, return NONE *)
-    val learner : t -> learner option
+    datatype msg =
+        Proposal of (
+                ballot *        (* ballot *)
+                hash            (* message hash *)
+                )
+        | NonProposal of (
+                acceptor *      (* sender *)
+                msg list *      (* references *)
+                msg option *    (* previous message *)
+                hash            (* message hash *)
+                )
+
+    type t = msg
+
+    fun hash (Proposal (_, h) | NonProposal (_, _, _, h)) = h
+
+    fun compute_hash (Proposal (bal, _)) =
+        Ballot.hash bal
+      | compute_hash (NonProposal (_, refs, prev, _)) =
+        let
+            val refs_hash = List.map hash refs
+            val prev_hash = map_or prev [] (fn p => [hash p])
+        in
+            prev_hash @ refs_hash |> Hashing.hash
+        end
 
-    (* returns message sender *)
-    val sender : t -> acceptor
+    (* TODO check if equality is used *)
+    fun eq (Proposal (_, h1), Proposal (_, h2)) = h1 = h2
+      | eq (NonProposal (_, _, _, h1), NonProposal (_, _, _, h2)) = h1 = h2
+      | eq (_, _) = false
 
-    (* if the message is 1a, return its ballot and value; otherwise, return NONE *)
-    val get_bal_val : t -> (ballot * value) option
+    (* fun typ (Msg (t, _, _, _, _)) = t *)
 
-    (* returns a previous message of the sender *)
-    val get_prev : t -> t option
+    fun is_proposal (Proposal _) = true
+      | is_proposal _ = false
 
-    (* returns a list of direct references *)
-    val get_refs : t -> t list
+    (* TODO this should be raw? *)
+    fun mk_non_proposal (sender, prev_msg, recent_msgs) =
+        let val hash = Word.fromInt 42 in
+            NonProposal (sender, recent_msgs, prev_msg, hash)
+        end
+
+    fun sender (NonProposal (sender, _, _, _)) = sender
+      | sender _ = raise Fail "sender not defined"
+
+    fun get_bal_val (Proposal (b, _)) =
+        let val v = Ballot.value b in SOME (b, v) end
+      | get_bal_val _ = NONE
+
+    fun get_prev (Proposal _) = NONE
+      | get_prev (NonProposal (_, _ , prev, _)) = prev
+
+    fun get_refs (Proposal _) = []
+      | get_refs (NonProposal (_, refs , _, _)) = refs
 end
 
 functor MessageOrdKey (Msg : HPAXOS_MESSAGE) : ORD_KEY =
@@ -72,15 +83,18 @@ 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)) *)
 
     fun references_exactly_one_1a m : bool =
         let fun check (x, (found, false)) = (found, false)
               | check (x, (false, true)) =
-                if Msg.is_one_a x then (true, true) else (false, true)
+                if Msg.is_proposal x then (true, true) else (false, true)
               | check (x, (true, true)) =
-                if Msg.is_one_a x then (true, false) else (true, true)
+                if Msg.is_proposal x then (true, false) else (true, true)
         in
             case foldl check (false, true) (Msg.get_refs m) of
                 (found, no_second) => found andalso no_second
@@ -101,8 +115,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 +143,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) =

hpaxos/hpaxos-value.sig

@@ -0,0 +1,7 @@
+signature HPAXOS_VALUE =
+sig
+    type t
+
+    val default : t (* default value *)
+    val eq : t * t -> bool (* equality *)
+end

hpaxos/hpaxos-value.sml

@@ -0,0 +1,7 @@
+structure HPaxosValue : HPAXOS_VALUE =
+struct
+    type t = word
+
+    val default = Word.fromInt 0
+    val eq : t * t -> bool = (op =)
+end