Quic fsm

include quic_types
include quic_frame

https://tools.ietf.org/html/draft-ietf-quic-transport-29#page-15

Since we want to represent the receiving FSM of the tested implementation, we will use these relations when WE sent frame infering the state of the opponant. We assume perfect reliability of the medium. However a more correct way would be to represent state when, we receive ACK for the corresponding frame but this would introduce some delay between the real current state of receiver and the represented one.

• For each stream id S, receiving_recv(S) indicates that a STREAM frame, either a STREAM_DATA_BLOCKED or that a bidirectional stream is send by the sender to the receiver. => We can check when we send these frame

relation receiving_recv(S:stream_id)

- For stream id S, receiving_sizeKnown(S) indicates that the stream transmitted to receiver on stream id S is finished (that is, a FIN frame has been sent). (+-stream_finished) => We can check that when we send STREAM+FIN

relation receiving_sizeKnown(S:stream_id)

- For stream id S, receiving_dataRecvd(S) indicates that the stream id S is finished and that all the data has been received => We can test by checking all ACK received meaning that receiver receive data

relation receiving_dataRecvd(S:stream_id)

- For each stream id S, receiving_dataRead(S) indicates that the stream transmitted to receiver on stream id S is read (that is, a RESET_STREAM frame has been sent). => We cannot test if the application has read all the data

relation receiving_dataRead(S:stream_id)

- For each stream id S, receiving_resetRecvd(S) indicates that the stream transmitted to receiver on stream id S is reset (that is, a RESET_STREAM frame has been sent). (+-stream_reset) => We assume that when we sent the RESET_STREAM

relation receiving_resetRecvd(S:stream_id)

- For each stream id S, receiving_resetRead(S) indicates that the reset stream transmitted to receiver on stream id S is read (that is, a RESET_STREAM frame has been sent). (+-stream_reset) => We cannot check (maybe check if stream is reset)

relation receiving_resetRead(S:stream_id)

lastest_stream_id_receiving(P) contains a list of stream_id that appear in a given packet_number P, allow us to track which packet are acked

instance idx_r : unbounded_sequence
instance arr_streamid_r : array(idx_r,stream_id)
function lastest_stream_id_receiving(P:pkt_num) : this.arr_streamid_r

lastest_pkt_num_receiving contains a list of pkt_num that appear in a given execution, allow us to track which packet are sent(received)

instance jdx_r : unbounded_sequence
instance arr_pkt_num_r : array(jdx_r,pkt_num)
function lastest_pkt_num_receiving : this.arr_pkt_num_r

Before a stream is created, all streams of the same type with lower- numbered stream IDs MUST be created. This ensures that the creation order for streams is consistent on both endpoints. TODO

Initial state

after init {
    receiving_recv(S)      := false;
    receiving_sizeKnown(S) := false;
    receiving_dataRecvd(S) := false;
    receiving_dataRead(S)  := false;
    receiving_resetRecvd(S):= false;
    receiving_resetRead(S) := false;
}
action handle_receiving_recv(id:stream_id,seq:pkt_num) = {
    if ~stream_frame_restransmitted(id) & ~sdb_frame_restransmitted(id) {

possible source state/transition: none set of non allowed state (useless ?) allowed: require ~receiving_sizeKnown(id) & ~receiving_dataRecvd(id) & ~receiving_dataRead(id) & ~receiving_resetRecvd(id) & ~receiving_resetRead(id);

        receiving_recv(id) := true;

call show_fsm_receiving_recv_event; call show_receiving_fsm_event(receiving_recv(id),receiving_sizeKnown(id),receiving_dataRecvd(id),receiving_dataRead(id),receiving_resetRecvd(id),receiving_resetRead(id));

    };
    lastest_stream_id_receiving(seq) := lastest_stream_id_receiving(seq).append(id);
    lastest_pkt_num_receiving := lastest_pkt_num_receiving.append(seq);
}

action handle_receiving_sizeKnown(id:stream_id,seq:pkt_num) = {
    if ~stream_frame_restransmitted(id) {

possible source state/transition require receiving_recv(id); set of non allowed state (useless ?) require ~receiving_dataRecvd(id) & ~receiving_dataRead(id) & ~receiving_resetRecvd(id) & ~receiving_resetRead(id);

        receiving_recv(id) := false;
        receiving_sizeKnown(id) := true;

call show_fsm_receiving_sizeKnown_event; call show_receiving_fsm_event(receiving_recv(id),receiving_sizeKnown(id),receiving_dataRecvd(id),receiving_dataRead(id),receiving_resetRecvd(id),receiving_resetRead(id));

    };
    lastest_stream_id_receiving(seq) := lastest_stream_id_receiving(seq).append(id);
    lastest_pkt_num_receiving := lastest_pkt_num_receiving.append(seq);
}

action handle_receiving_dataRecvd(id:stream_id) = {

possible source state/transition require receiving_sizeKnown(id) | receiving_resetRecvd(id); set of non allowed state require ~receiving_dataRead(id) & ~receiving_resetRead(id);

    receiving_sizeKnown(id) := false;
    receiving_resetRecvd(id):= false;
    receiving_dataRecvd(id) := true;

call show_fsm_receiving_dataRecvd_event; call show_receiving_fsm_event(receiving_recv(id),receiving_sizeKnown(id),receiving_dataRecvd(id),receiving_dataRead(id),receiving_resetRecvd(id),receiving_resetRead(id));

}

action handle_receiving_dataRead(id:stream_id) = {

possible source state/transition require receiving_dataRecvd(id); set of non allowed state require ~receiving_dataRead(id) & ~receiving_resetRead(id) & ~receiving_resetRead(id);

    receiving_dataRecvd(id) := false;
    receiving_dataRead(id)  := true;

call show_fsm_receiving_dataRead_event; call show_receiving_fsm_event(receiving_recv(id),receiving_sizeKnown(id),receiving_dataRecvd(id),receiving_dataRead(id),receiving_resetRecvd(id),receiving_resetRead(id));

}

action handle_receiving_resetRecvd(id:stream_id,seq:pkt_num) = {
    if ~reset_frame_restransmitted(id) {

possible source state/transition require receiving_recv(id) | receiving_sizeKnown(id) | receiving_dataRecvd(id); set of non allowed state require ~receiving_resetRead(id) & ~receiving_dataRead(id);

        receiving_recv(id) := false;
        receiving_sizeKnown(id) := false;
        receiving_dataRecvd(id) := false;
        receiving_resetRecvd(id):=  true;

call show_fsm_receiving_resetRecvd_event; call show_receiving_fsm_event(receiving_recv(id),receiving_sizeKnown(id),receiving_dataRecvd(id),receiving_dataRead(id),receiving_resetRecvd(id),receiving_resetRead(id));

    };
    lastest_stream_id_receiving(seq) := lastest_stream_id_receiving(seq).append(id);
    lastest_pkt_num_receiving := lastest_pkt_num_receiving.append(seq);
}

action handle_receiving_resetRead(id:stream_id) = {

possible source state/transition require receiving_resetRecvd(id); set of non allowed state require ~receiving_sizeKnown(id) & ~receiving_dataRecvd(id) & ~receiving_dataRead(id);

    receiving_resetRecvd(id) := false;
    receiving_resetRead(id)  := true;

call show_fsm_receiving_recv_event; call show_receiving_fsm_event(receiving_recv(id),receiving_sizeKnown(id),receiving_dataRecvd(id),receiving_dataRead(id),receiving_resetRecvd(id),receiving_resetRead(id));

}

==================================================================== Auxilary functions =====================================================================

largest ack

action handle_receiving_ack(largest_acked:pkt_num) = {
    var jdx_r : jdx_r := 0;

call show_fsm_receiving_ack_event;

    while jdx_r < lastest_pkt_num_receiving.end {
        var seq := lastest_pkt_num_receiving.value(jdx_r);
        var idx_r : idx_r := 0;
        while seq <= largest_acked & idx_r < lastest_stream_id_receiving(seq).end {
            var sid := lastest_stream_id_receiving(seq).value(idx_r);
            if receiving_resetRecvd(sid) {
                call handle_receiving_resetRead(sid);
            } else if receiving_sizeKnown(sid) {
                call handle_receiving_dataRecvd(sid);
            };
            idx_r := idx_r.next;
        };
        jdx_r := jdx_r.next;
    };
}


import action show_receiving_fsm_event(receiving_recv:bool,receiving_sizeKnown:bool,
                                       receiving_dataRecvd:bool,receiving_dataRead:bool,
                                       receiving_resetRecvd:bool,receiving_resetRead:bool)

import action show_fsm_receiving_recv_event

import action show_fsm_receiving_sizeKnown_event

import action show_fsm_receiving_dataRecvd_event

import action show_fsm_receiving_dataRead_event

import action show_fsm_receiving_resetRecvd_event

import action show_fsm_receiving_resetRead_event

import action show_fsm_receiving_ack_event