[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] TCP/IP client/server communication protocol



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.