Re: [tlaplus] TCP/IP client/server communication protocol

The main question you should consider is if including clocks in your TLA+ model is necessary for the properties you wish to verify. Including clocks inevitably blows up your state space, and it may be enough to consider that an action triggered by a timeout may non-deterministically occur at any time during the execution. This is clearly an over-abstraction and may therefore lead to spurious counter-examples where the timeout occurs "too soon", but you can try to rule out those counter-examples by adding enabling conditions to your actions. (In particular, these conditions may refer to variables that are not visible to the process in the implementation of your system, they express global synchronization conditions that are ensured by the timers in your implementation.)

[1] https://groups.google.com/forum/#!topic/tlaplus/mvrg99_xc74

On 3 Mar 2020, at 21:42, Emanuel Koczwara <emanuel.koczwara@xxxxxxxxx> wrote:

Hi,

I'm trying to write a specification for an existing system.

I have a server and clients connected through TCP/IP (this is oversimplification, in fact I use ZMQ and IPC channels also can be used).

The protocol is based on serialized C++ structures (protocol bufferes, cereal, whatever, not important, lets abstract that away).

I have couple of questions:

1. How to handle time, timers and timeouts?

I have a monotonic clock on each node (each client and the server). I have implemented a heartbeat. Ping/pong message contains current time. This is what I have at the moment:

ClientStateType ==
[ clock : Nat
, timeout : Nat
, pingResponse : Nat
, interval : Nat
, pingRequest : Nat
... other fields ...
]

ClientInitialState ==
[ clock |-> 0
, timeout |-> 0
, pingResponse |-> 0
, interval |-> 0
, pingRequest |-> 0
... other fields ...
]

ServerTick ==
/\ server' = [ server EXCEPT !.clock = @ + 1 ]

ClientTick ==
/\ client' = [ client EXCEPT !.clock = @ + 1 ]

Next ==
\/ ServerTick
\/ ClientTick
... other actions ...

Is this approach correct?

2. In my API I have setters and gettes. By getters I mean methods/functions that just returns a value, for example:

/// Setup heartbeat.
/**
@param interval How often send PingRequest.
@param timeout How long wait for PingReply.

@warning Should be called before Api::connect or Api::connectAndWait
*/
void setupHeartbeat(uint32_t interval, uint32_t timeout);

/// Get current heartbeat interval.
uint32_t heartbeatInterval() const;

/// Get current heartbeat timeout.
uint32_t heartbeatTimeout() const;

I would like to include heartbeatInterval and heartbeatTimeout in my specification for completness, but I have no idea how these definitions should look like. I can just use UNCHANGED << all my variables >> in definitions, but that feels wrong - useless.

3. My API is based on async handlers. For example I have this:

/// Send SyncVersionInfoRequest message.
/**
@note Async action.
*/
void getVersionInfo(const std::function<void(Error error, std::string info)> &handler);

Info handler is stored in private vector of handlers and it is called when the response is received.

void Api::handleGetVersionInfoResponse(const SyncGetVersionInfoResponse &msg)
{
if(_getVersionInfoResponseHandlers.count(msg.msg) > 0)
{
_getVersionInfoResponseHandlers[msg.msg]({ErrorType::NONE, {}, {}}, msg.data);
_getVersionInfoResponseHandlers.erase(msg.msg);
return;
}

handleUnexpectedResponse();
}

How to model these calls? How to model my handlers? Maybe something like simple counters would do? I would like to know the most common approach.

4. Is there an example of this kind of system/API backed up with implementation?

Thanks,
Emanuel

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5438ad7f-ae93-4a19-be61-e78a67d29560%40googlegroups.com.