Safety Property: NetHardBandwidthLimit

property NetHardBandwidthLimit (bLimit: int, tLimit: int) {
  // Limit network bandwidth useage to nbytes every timeStep (in milliseconds)
  // Hard limit means that an error is reported whenever the limit is
  // exceeded.
  requires NetworkTotalBandwidthCounter;

  helper NetHardBandwidthLimitCheck (nbytes: int, bytesLeft: int,
                                     byteLimit: int, timeSlice: int,
                                     isSend: boolean) {
    if (bytesLeft < nbytes) {
      violation ("Maximum network " + (isSend ? "send" : "receive") + 
                 " bandwidth exceeded.  Maximum of " +
                 byteLimit + " bytes per " + timeSlice +
                 " millisecond timeslice.  " + (byteLimit - bytesLeft) +
                 " bytes already used this timeslice. " +
                 (isSend ? "Attempting to send " : "About to receive ") +
                  nbytes + " bytes.");
    }
  }

  check RNetwork.initialize () {
    sendTimeSlice = tLimit;
    receiveTimeSlice = tLimit;
    totalByteLimit = bLimit;
    totalBytesLeft = bLimit;
  }
  
  check RNetwork.preSend (remote: RNetAddress, nbytes: int) {
    NetHardBandwidthLimitCheck (nbytes, totalBytesLeft, totalByteLimit,
                                sendTimeSlice, true);
  }

  check RNetwork.preReceive (remote: RNetAddress, nbytes: int) {
    NetHardBandwidthLimitCheck (nbytes, totalBytesLeft, totalByteLimit,
                                receiveTimeSlice, false);
  }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science