Alternating Bit Protocol

VI.9 Alternating Bit Protocol

Alternating Bit Protocol: Intro [Slide 236]

Implementations of the message-passing model, such as TCP/IP, provide the programmer with an abstraction of a stream of data messages sent from process A to process B such that each message is delivered in the order sent.
However, the physical communication between A and B is not necessarily completely reliable. Due to congestion in the network (other traﬃc), transient noise, buﬀer overﬂows, or other problems, some of the messages sent out over the network from process A may not actually arrive at process B, or they may arrive incomplete or corrupted (usually detected with a checksum).

Therefore, it is necessary to include in these message-passing implementations a protocol that ensures that when a message is lost, it is retransmitted by the sender.
At the same time, the protocol must guarantee that duplicate messages are not delivered to the receiver and that the delivery order is consistent with the sending order.
We will study the alternating bit protocol, a simple yet eﬀective protocol for managing the retransmission of lost messages.

A: sender process
B: receiver process
D: channel to send data from A to B
ACK: channel to send acknowledgements from B to A indicating whether data received was corrupted or not.

Protocol managing retransmissions

1.: when message is lost then retransmission by the sender
2.: sending order is consistent with receiving order

For sender A and receiver B the alternating bit protocol is as follows

Each data message sent by A contains a protocol bit, 0 or 1.
When A sends a message, it sends it repeatedly (with its corresponding bit) until receiving an acknowledgement (ACK) from B that contains the same protocol bit as the message being sent.
When B receives a message, it sends an ACK to A and includes the protocol bit of the message received. The ﬁrst time the message is received, the protocol delivers the message for processing. Subsequent messages with the same bit are simply acknowledged.
When A receives an acknowledgement containing the same bit as the message it is currently transmitting, it stops transmitting that message, ﬂips the protocol bit, and repeats the protocol for the next message.

Alternating Bit Protocol V1 [Slide 240]

Introduce the alternating bit protocol in stages
Both D and ACK are not lossy

Tempura code:

load "tam". 
/∗ tam provides an api for defining channels and 
   provides the synchronous receive and send commands: 
   chan(C)  : defines a channel C 
   wrc(C,X) : send the value of X over channel C 
   rdc(C,V) : receive the value V over channel C 
   ready(C) : there is data in channel C 
∗/

/∗ run ∗/ define abp() = { 
  exists D, Ack : { 
  /∗ D  : channel used to send and receive data 
     Ack: channel used to send and receive acknowledgements 
   ∗/ 
 
  /∗ main body of the system, declare 2 channels and 
     let the sender and receiver communicate via those channels ∗/ 
  len(20) and chan(D) and chan(Ack) and 
  sender(D,Ack) and receiver(D,Ack) 
  } 
}.

/∗ the sender ∗/ 
define sender(D,Ack) = { 
  exists Sendbuff, Data, RAck : { 
    /∗ Sendbuff: variable containing data to be sent, 
       Data    : variable used in the generation of data 
       RAck    : variable used to store the received Ack 
    ∗/ 
    define no_data = -2 and /∗ indicates no data in Sendbuff ∗/ 
 
    /∗ function indicating whether Sendbuff contains data or not ∗/ 
    define new_data() = { Sendbuff ~= no_data } and 
 
    /∗ generate data and put it in Sendbuff ∗/ 
    define produce() = { 
      format("A is producing                           %t\n", Data) 
      and  Data := Data + 1 and Sendbuff:= Data 
    } and

    /∗ send data in Sendbuff via channel D ∗/ 
    define sendD() = { 
      format("A is sending    via D   %t\n", Sendbuff) and 
      wrc(D,Sendbuff) 
    } and 
 
    /∗ receive Ack and put it in RAck ∗/ 
    define recAck() = { 
      rdc(Ack,RAck) and 
      format("A is receiving  via Ack %t\n",RAck) and 
      Sendbuff := no_data 
    } and 
 
    /∗ initial state: Sendbuff contains no data and Data is zero ∗/ 
     Sendbuff = no_data and  Data = 0 and 
 
    /∗ show in each state the value of Sendbuff ∗/ 
    always format("A, Sendbuff=%d\n",Sendbuff) and

    /∗ main body of the sender ∗/ 
    chopstar{ skip and 
      if new_data() then { sendD() and recAck() and stable(Data) } 
                    else { produce() } 
    } 
  } 
}.

/∗ the receiver ∗/ 
define receiver(D,Ack) = { 
  exists RData : { 
   /∗ RData: used to store the received data from channel D ∗/ 
 
   /∗ receive data from channel D and store it in RData ∗/ 
   define recD() = { 
     rdc(D,RData) and 
     format("B is receiving  via D   %t\n",RData) and 
     format("B is consuming                           %t\n", RData) 
   } and 
 
   /∗ send 1 via channel Ack ∗/ 
   define sendAck() = { 
     wrc(Ack, 1) and 
     format("B is sending    via Ack %t\n",1) 
   } and

   /∗ main body of the receiver ∗/ 
   chopstar{ skip and 
      if ready(D) then { recD() and sendAck() } 
   } 
  } 
}.

Alternating Bit Protocol V2 [Slide 247]

D is lossy and ACK is not lossy

Tempura code:

load "tam". 
/∗ tam provides an api for defining channels and 
   provides the synchronous receive and send commands: 
   chan(C)  : defines a channel C 
   wrc(C,X) : send the value of X over channel C 
   rdc(C,V) : receive the value V over channel C 
   ready(C) : there is data in channel C 
∗/

/∗ run ∗/ define abp() = { 
  exists D, Ack : { 
   /∗ D  : lossy channel used to send and receive data 
      Ack: channel used to send and receive acknowledgements 
   ∗/ 
 
  /∗ main body of the system, declare 2 channels and 
     let the sender and receiver communicate via those channels ∗/ 
  len(20) and chan(D) and chan(Ack) and 
  sender(D,Ack) and receiver(D,Ack) 
  } 
}.

/∗ the sender ∗/ 
define sender(D,Ack) = { 
 exists Sendbuff, Data, RAck : { 
    /∗ Sendbuff: variable containing data to be sent, 
       Data    : variable used in the generation of data 
       RAck    : variable used to store the received Ack 
    ∗/ 
    define no_data = -2 and /∗ indicates no data in Sendbuff ∗/ 
 
    define faulty_s_data = -1 and /∗ indicates faulty sent data ∗/ 
 
    /∗ function indicating whether Sendbuff contains data or not ∗/ 
    define new_data() = { Sendbuff ~= no_data } and 
 
    /∗ generate data and put it in Sendbuff ∗/ 
    define produce() = { 
      format("A is producing                           %t\n", Data) 
      and  Data := Data + 1 and Sendbuff:= Data 
    } and

    /∗ send data in Sendbuff via lossy channel D ∗/ 
    define sendD() = { 
      format("A is sending    via D   %t\n", Sendbuff) and 
      if Random mod 2 = 1 then { wrc(D,Sendbuff) } 
                          else { wrc(D,faulty_s_data) } 
    } and 
 
    /∗ receive Ack and put it in RAck 
       if RAck is zero then Sendbuff needs to be sent again ∗/ 
    define recAck() = { 
      rdc(Ack,RAck) and 
      format("A is receiving  via Ack %t\n",RAck) and 
      if RAck ~= 0 then { 
          Sendbuff := no_data and 
          format("A, Ack is ok \n") 
      } else { 
          Sendbuff := Sendbuff and 
          format("A, Ack is not ok, resending \n") 
      } 
     } and

   /∗ initial state: Sendbuff contains no data and Data is zero ∗/ 
   Sendbuff = no_data and  Data = 0 and 
 
   /∗ show in each state the value of Sendbuff ∗/ 
   always format("A, Sendbuff=%d\n",Sendbuff) and 
 
   /∗ main body of the sender ∗/ 
   chopstar{ skip and 
     if new_data() then { sendD() and recAck() and stable(Data) } 
                   else { produce() } 
   } 
 } 
}.

/∗ the receiver ∗/ 
define receiver(D,Ack) = { 
 exists RData : { 
 /∗ RData: variable used to store the received data from channel D ∗/ 
  define faulty_r_data = -1 and /∗ indicates faulty received data ∗/ 
  /∗ receive data from lossy channel D and store it in RData 
     if data is not faulty send 1 via channel Ack 
     if data is faulty send 0 via channel Ack ∗/ 
  define recDsendAck() = { 
    rdc(D,RData) and 
    format("B is receiving  via D   %t \n", RData) and 
    if RData ~= faulty_r_data then { 
      format("B is consuming                           %t \n", RData) 
      and format("B is sending    via Ack %t \n",1) and 
      wrc(Ack, 1) 
    } else { 
       format("B, Data over D is lost \n") and 
       format("B is sending    via Ack %t\n",0) and 
       wrc(Ack, 0) 
    } 
  } and

  /∗ main body of the receiver ∗/ 
  chopstar{ skip and 
        if ready(D) then { recDsendAck() } 
  } 
 } 
}.

Alternating Bit Protocol V3 [Slide 254]

Both D and ACK are lossy

Tempura code:

load "tam". 
/∗ tam provides an api for defining channels and 
   provides the synchronous receive and send commands: 
   chan(C)  : defines a channel C 
   wrc(C,X) : send the value of X over channel C 
   rdc(C,V) : receive the value V over channel C 
   ready(C) : there is data in channel C 
∗/

/∗ run ∗/ define abp() = { 
  exists D, Ack : { 
   /∗ D  : lossy channel used to send and receive data 
      Ack: lossy channel used to send and receive acknowledgements 
   ∗/ 
 
  /∗ main body of the system, declare 2 channels and 
     let the sender and receiver communicate via those channels ∗/ 
  len(20) and chan(D) and chan(Ack) and 
  sender(D,Ack) and receiver(D,Ack) 
  } 
}. 
 
define flip(X) = { if X=1 then 0 else 1 }.

/∗ the sender ∗/ 
define sender(D,Ack) = { 
 exists Sendbuff, Data, RAck, Cs : { 
  /∗ Sendbuff: variable containing data to be sent, 
     Data    : variable used in the generation of data 
     RAck    : variable used to store the received Ack 
     Cs      : variable containing the current protocol bit 
   ∗/ 
  define no_data = -2 and /∗ indicates no data in Sendbuff ∗/ 
  define faulty_s_data = [-1,-1] and /∗ indicates faulty sent data ∗/ 
  define faulty_r_ack = -1 and /∗ indicates faulty received ack ∗/ 
 
  /∗ function indicating whether Sendbuff contains data or not ∗/ 
  define new_data() = { Sendbuff ~= no_data } and 
 
  /∗ generate data and put it in Sendbuff 
     update the protocol bit in Cs ∗/ 
  define produce() = { 
    format("A is producing                           %t\n", Data) and 
    Cs := flip(Cs) and Data := Data + 1 and Sendbuff:= Data 
  } and

  /∗ send data in Sendbuff via lossy channel D ∗/ 
  define sendD() = { 
    format("A is sending    via D   %t\n", [Sendbuff,Cs]) and 
    if Random mod 2 = 1 then { wrc(D,[Sendbuff,Cs]) } 
                        else { wrc(D,faulty_s_data) } 
  } and

  /∗ receive Ack and put it in RAck 
     if RAck is not faulty and is equal to protocol bit Cs 
     then Sendbuff is updated 
     if RAck is not faulty and is not equal to protocol bit Cs 
     then Sendbuff needs to be sent again 
     if RAck is faulty then Sendbuff needs to be sent again 
   ∗/ 
  define recAck() = { 
    rdc(Ack,RAck) and 
    format("A is receiving  via Ack %t\n",RAck) and 
    if RAck ~= faulty_r_ack then { 
      if Cs = RAck then { 
        Sendbuff := no_data and format("A, Ack is ok \n") 
      } else { 
        Sendbuff:=Sendbuff and format("A, Ack is not ok, resending\n") 
      } 
    } else { 
        Sendbuff:=Sendbuff and format("A, Ack is lost, resending \n") 
    } 
  } and

  /∗ initial state: Sendbuff contains no data and Data is zero 
     protocol bit Cs is zero ∗/ 
  Sendbuff = no_data and  Data = 0 and Cs = 0 and 
 
  /∗ show in each state the value of Sendbuff and protocol bit Cs∗/ 
  always format("A, Sendbuff=%d, Cs=%d\n",Sendbuff,Cs) and 
 
  /∗ main body of the sender ∗/ 
  chopstar{ skip and 
    if new_data() then { sendD() and recAck() and 
                                      stable(Data) and stable(Cs) } 
                  else { produce() } 
  } 
 } 
}.

/∗ the receiver ∗/ 
define receiver(D,Ack) = { 
  exists RData,
Cr : { 
   /∗ RData: variable used to store the received data from channel D 
      Cr   : variable containing the current protocol bit 
    ∗/ 
 
   define faulty_r_data = -1 and /∗ indicates faulty received data ∗/ 
   define faulty_s_ack = -1 and /∗ indicates faulty sent ack ∗/ 
 
   /∗ send over lossy channel Ack the value X ∗/ 
   define lossy_ack_send(X) = { 
     if Random mod 2 = 1 then { wrc(Ack, X) } 
                         else { wrc(Ack,faulty_s_ack) } 
   } and

  /∗ receive data from lossy channel D and store it in RData 
     if received data is not faulty and is equal to protocol bit Cr 
     then send via Ack protocol bit Cr and update Cr 
     if received data is not faulty and 
        is not equal to protocol bit Cr 
     then send via Ack the complement of protocol bit Cr 
     if received data is faulty then send via Ack the complement of 
     protocol bit Cr 
   ∗/ 
   define recDsendAck() = { 
     rdc(D,RData) and 
     format("B is receiving  via D   %t\n",RData) and 
     /∗ !!! provide the missing bit here ∗/ 
   } and

   /∗ initialise protocol bit Cr to 1 ∗/ 
   Cr = 1 and 
 
   /∗ show in each state the value of protocol bit Cr ∗/ 
   always format("B, Cr=%d \n",Cr) and 
 
   /∗ main body of the receiver ∗/ 
     chopstar{ skip and 
        if ready(D) then { recDsendAck() } 
                    else { stable(Cr) } 
     } 
    } 
}.

2023-09-12