From 19a645e6f2fff4110c737f7cbe11788b96595fad Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 17 Mar 2017 16:38:26 -0700 Subject: [PATCH] repstore2 and repstore2bug are working --- doc/examples/testing/repstore2bug.ivy | 522 ++++++++++++++++++++++++++ 1 file changed, 522 insertions(+) create mode 100644 doc/examples/testing/repstore2bug.ivy diff --git a/doc/examples/testing/repstore2bug.ivy b/doc/examples/testing/repstore2bug.ivy new file mode 100644 index 0000000..93437e2 --- /dev/null +++ b/doc/examples/testing/repstore2bug.ivy @@ -0,0 +1,522 @@ +#lang ivy1.6 + +# Exercise: A buggy replicating key-value store +# ============================================= +# +# In this version of the [replicating key-value +# store](repstore2.html), we've added a bug as an exercise. Try to +# find the bug using compositional testing (don't use diff, it's too +# easy). Fix the bug and test again. +# +# ### Bonus exercise +# +# At the end of the file, there is an isolate `iso_sys` that includes +# the complete implmentation (including both servers and the +# network). Try testing this isolate to see if you can find error. +# If not, can you explain why not? + +# Change the interpretation of type `key` to give it a larger range (say, `strbv[4]`). +# Try testing isolates `iso_prim` and `iso_sec`. Do you still find the bug. If not, +# can you explain why not? + +# Basic data types +# ---------------- + +# As with he simple one-process server (see +# [repstore1.ivy](repstore1.html)), we begin by declaring the data +# types needed to represent transactions and the messages that carry +# them. + +# The key and value types are uninterpreted for the moment. + + +type key +type value +ghost type txid + +type request_kind = {write,read} + +object request_body = { + type t = struct { + knd : request_kind, + ky : key, + vl : value + } +} + +object request = { + type t = struct { + tx : txid, + bd : request_body.t + } +} + +object response_body = { + type t = struct { + vl : value + } +} + +object response = { + type t = struct { + tx : txid, + bd : response_body.t + } +} + +# The definition of a replica is also the same as before. + +module replica = { + function store(K:key) : value + after init { + store(K) := 0 + } + action exec(inp : request_body.t) returns (out:response_body.t) = { + if inp.knd = write { + store(inp.ky) := inp.vl; + } + else if inp.knd = read { + out.vl := store(inp.ky); + } + } +} + +# The first difference is that we now have two servers, so the +# enumerated type `dest.t` has two values, one for the primary and one +# for the secondary. + +object dest = { + ghost type t = {prim,sec} +} + +# Reference object +# ---------------- + +# Our reference model is the same as before. + +object ref = { + action create(inp : request_body.t, dst:dest.t) returns (tx : txid) + action commit(tx : txid,dst:dest.t) + action eval(tx : txid) returns (res : response_body.t) + + instance rep : replica + + individual next : txid + function txs(X:txid) : request_body.t + function txres(X:txid) : response_body.t + relation committed(X:txid) + + after init { + next := 0; + committed(X) := false; + } + + implement create { + tx := next; + txs(tx) := inp; + next := next + 1; + } + + implement commit { + assert 0 <= tx & tx < next; + assert ~committed(tx); + txres(tx) := rep.exec(txs(tx)); + committed(tx) := true; + } + delegate commit + + implement eval { + assert committed(tx); + res := txres(tx); + } + delegate eval + + interpret txid -> int +} + + + +# This time, however, we'll add another reference object to keep track +# of the serialization order, so we can specify the interface between +# primary and secondary. It has one action `serialize` that indicates when +# a write transaction is serialized. + +object ser = { + + action serialize(tx : txid) + + # The serializer object keeps track of which transactions have + # been serialized. + + relation serialized(X:txid) + + after init { + serialized(X) := false; + } + + # To serialzie a write, we must guarantee that transaction exists, + # and that it has not already been serialized. Further, we can + # only serialize write transactions. + + implement serialize { + assert 0 <= tx & tx < ref.next; + assert ~serialized(tx); + assert ref.txs(tx).knd = write; + serialized(tx) := true; + } + delegate serialize + + # Further,we specify that a write transaction cannot be committed + # until it is serialized. + + before ref.commit(tx : txid,dst:dest.t) { + assert ref.txs(tx).knd = write -> serialized(tx); + } +} + +# The implementation +# ------------------ + +# Now we are ready to define our system implemention, consisting of +# client endpoints, the primary server and the secondary server. + +# Notice we include the `tcp` module here, since we will need it for +# the ordered channels between the servers. + +include tcp +include udp + +# Again, we have an uninterpreted type of client ids, and a request +# message structure that encapsulates the request with its client id +# for routing the response. + +type client_id + +type req_msg = struct { + cid : client_id, + req : request.t +} + +# The client endpoint is the same as before, except that we now have +# two servers, so the client must decide which of the servers to send +# a request to. + +module client(cid,prim_chan,sec_chan,cl_chans) = { + + action client_request(req : request_body.t, the_dst: dest.t) + action client_response(req : response_body.t, tx : txid) + + # To generate a request, we build a request message and send it to + # the server. The server endpoint we send to is determined by the + # parameter `the_dst`. + + implement client_request { + local m : req_msg { + m.cid := cid; + m.req.tx := ref.create(req,the_dst); + m.req.bd := req; + if the_dst = dest.prim { + call prim_chan.send(m); + } else { + call sec_chan.send(m); + } + } + } + + # To handle a response from the server, we simply pass it to the + # `client_response` callback. The transaction id parameter is + # "ghost" and is only used for specification. + + implement cl_chans.recv(resp : response.t) { + call client_response(resp.bd,resp.tx) + } +} + +# The primary server module now has two additional parameters, for the +# forward channel (forwarding writes to the secondary) and the reverse +# channel (returning acks). + +module primary_node(port, fwd_chan, rev_chan, cl_chans) = { + instance rep : replica + + # Again, we have an endpoint for receiving requests from clients. + + instance req_chan : nondup_endpoint(port,req_msg) + + # We have to remember how many pending writes each key has. We use + # a map from keys to counters for this. + + instance counter : unbounded_sequence + function pending(K:key) : counter.t + + # Initially, all the counters are zero. + + after init { + pending(K) := 0; + } + + # When receiving a request message from a client, the primary + # node must first check whether it is a read or a write. In the case + # of a read, we check if the key has a pending write. If not, we commit + # the read, execute it, and return the response to the client. If there is + # a pending write, we postpone the read by forwarding it to ourself. In + # case of a write, we serialize the write, forward it to the secondary, + # increment the pending count of the key, and finally execute it. + # + + implement req_chan.recv(inp : req_msg) { + var rr := inp.req.bd; + if rr.knd = read { + if pending(rr.ky) = 0 { + call ref.commit(inp.req.tx,dest.prim); + var res : response.t; + res.tx := inp.req.tx; + res.bd := rep.exec(rr); + call cl_chans(inp.cid).send(res) + } else { + call req_chan.send(inp); # if cannot execute, recirculate + } + } else if rr.knd = write { + call ser.serialize(inp.req.tx); # this is ghost! + call fwd_chan.send(inp); + var res := rep.exec(inp.req.bd); + } + } + + # When we receive a write request on the acknowledgement channel, + # we decrement the pending count of the key. + + implement rev_chan.recv(inp : req_msg) { + var rr := inp.req.bd; + if rr.knd = write { + pending(rr.ky) := pending(rr.ky).prev; + } + } +} + +# The secondary server handles only read request from clients. Since +# the secondary's replica refelects only committed writes, we cann +# immediately response to a read. We commit the read, build a response +# message by executing the read on the replica, and send the response +# back to the client. + +module secondary_node(port, fwd_chan, rev_chan, cl_chans) = { + instance rep : replica + + instance req_chan : nondup_endpoint(port,req_msg) + + implement req_chan.recv(inp : req_msg) { + var rr := inp.req.bd; + if rr.knd = read { + call ref.commit(inp.req.tx,dest.sec); + var res : response.t; + res.tx := inp.req.tx; + res.bd := rep.exec(rr); + call cl_chans(inp.cid).send(res); + } + # ignore writes! + } + + # When the secondary receives a forwarded write from the primary, + # it commits it, executes it, and sends the response to the + # client. + # + + implement fwd_chan.recv(inp : req_msg) { + var res : response.t; + res.tx := inp.req.tx; + res.bd := rep.exec(inp.req.bd); + call cl_chans(inp.cid).send(res); + call rev_chan.send(inp); + } + +} + +# The plumbing +# ------------ + +# Now we two servers, a primary and a secondary, and an array of +# client endpoints, connecting them up with network channels. + +# We have two TCP (ordered) channels beteween the primary and +# secondary, one forward (listening on port 44090) and one reverse +# (listening on port 44091). Both carry request messages. + +instance fwd_chan : tcp_channel("localhost:44090",req_msg) +instance rev_chan : tcp_channel("localhost:44091",req_msg) + +# As before, we use a parameterized array of (unordered) endpoints for +# the clients called `cl_chans`. The endpoints will use a range of +# port numbers beginning with `441000`. + +instance cl_chans : nondup_endpoint_set(client_id,44100,response.t) + +# We create a corresponding array of clients. +instance cl(X:client_id) : client(X,prim.req_chan,sec.req_chan,cl_chans) + +# We create the primary and secondary servers, connecting them with +# channels. The port numbers are for the client request channels of +# the servers. + +instance prim : primary_node(44200,fwd_chan.sndr,rev_chan.rcvr,cl_chans) +instance sec : secondary_node(44201,fwd_chan.rcvr,rev_chan.sndr,cl_chans) + +# The interface specifications +# ---------------------------- + +# The service specification is unchanged from the simple sequential +# server. + +object service_spec = { + + relation responded(X:txid) + + after init { + responded(X) := false; + } + + before cl_chans.send(p : client_id, m : response.t) { + assert ~responded(m.tx); + assert m.bd = ref.eval(m.tx); + responded(m.tx) := true; + } +} + +# Now, however, we need a specification for the interface between the +# primary and the secondary. This will allow us to test the two +# servers in isolation. We call this specification `mid_spec`. The state +# of this interface keeps a FIFO queue of messages that have been serialized +# but not yet transmitted over the interface. When a message is serialize, +# we insert it in this queue + +object mid_spec = { + instance queue : unbounded_queue(txid) + + after ser.serialize(tx:txid) { + call queue.push(tx); + } + + # When a message is received at the secondary on the forward + # channel, its contents must be correct for the given transaction + # id. Moreover, the transaction id must be the next on in the + # FIFO queue (in other words, the writes must arrive in + # serialization order). To make things a little easier, we commit + # the message when it is received. This gurantees that commits + # from the secondary always occur in order, without our having to + # explicitly specify that. Because the commit operation is + # "ghost", it doesn't matter whether we execute in implementation + # or specification code. We can put it wherever it is most + # convenient. + + before fwd_chan.rcvr.recv(inp : req_msg) { + assert inp.req.bd = ref.txs(inp.req.tx); + assert inp.req.tx = queue.pop; + call ref.commit(inp.req.tx,dest.sec); + } + + # This tells IVy that the above specification is a guarantee for + # the primary server, not for the network, which is the actual + # caller of `fwd_chan.rcvr.recv`. This means that the assertions + # will be verified when we test the primary. Usually, IVy's + # default assignment of guarantees to object is what we want, but + # in this case the caller is not the guarantor of the assertions. + + delegate fwd_chan_rcvr_recv[before] -> prim + + # The interface also requires that a given write message be acked + # at most once. Otherwise, the pending counts in the primary will + # be wrong. To ensure this, we maintain a set `acked` of + # acknowledgef transactions. + + relation acked(X:txid) + + after init { + acked(X) := false; + } + + # When an ack message is sent on the reverse channel, it must have + # been committed (this is the meaning of the message) and it must + # not already be acked. We record the fact that it is now acked. + + before rev_chan.sndr.send(inp : req_msg) { + assert ref.committed(inp.req.tx); + assert ~acked(inp.req.tx); + acked(inp.req.tx) := true; + } + + # When a request is created, we record the destination server. In + # this way we can determine which server is allowed to commit the + # request. This is a very common situation in specifications of + # distributed services. Much of the interface state tends to be + # related to the question of who is allowed to commit shich + # transations. + + function req_dest(X:txid) : dest.t + + after ref.create(inp : request_body.t, dst:dest.t) returns (tx : txid) { + req_dest(tx) := dst + } + + # We now specify that all reads must be commited by the server + # they are addressed to, while all writes are committed by the + # secondary + + before ref.commit(tx : txid,dst:dest.t) { + assert ref.txs(tx).knd = read -> req_dest(tx) = dst; + assert ref.txs(tx).knd = write -> dst = dest.sec + } + + +} + +# We export/import our API. + +export cl.client_request +import cl.client_response + +# Finally, we create two isolates the allow us to verify our two +# servers in isolation. Each isolate verifies just the the guarentees +# of given server, either the primary or secondary. In both cases we +# use our interface specifications and our reference object. The other +# server and the network are abstracted away. Their role is played by +# the test generator. Because we placed our interface specification +# `mid_spec` at the secondary end of the channels `fwd_chan` and +# `rev_chan`, those channels are used in the primary's isolate, but +# not in the secondary's. Notice also that the client endpoints `cl` +# are present in both isolates. Since they are trivial "stubs", there +# is no reason to separate them into their own isolate. + +trusted isolate iso_prim = prim with cl,cl_chans,ref,ser,service_spec,mid_spec,fwd_chan,rev_chan +trusted isolate iso_sec = sec with cl,cl_chans,ref,ser,service_spec,mid_spec + +# Here is an extra isolate you can use for integration testing: + +trusted isolate iso_sys = this + +# As before, we have to give concrete interpretations for the abstract +# types in order to test. + +interpret txid -> int +interpret key -> strbv[1] +interpret value -> bv[16] +interpret client_id -> bv[1] + +# The source file for this example is [here](repstore2.ivy). Try running this +# example using commands like this: +# +# $ ivy_to_cpp target=test isolate=iso_prim build=true repstore2.ivy +# $ ./repstore1 iters=100 runs=10 out=file.iev +# +# This tests the primary server. Look at the trace file `file.iev` +# and notice which actions are generated by the tester and which by +# the code. +# +# To test the secondary, use these commands: +# +# $ ivy_to_cpp target=test isolate=iso_sec build=true repstore2.ivy +# $ ./repstore1 iters=100 runs=10 out=file.iev +# +# Again, see what actions the tester is generating. Try putting some +# errors in this example and see if they produce assertions +# failures. If not, why not? +#