www.prismmodelchecker.org

Simple Peer-To-Peer Protocol

Contents

Introduction

This case study describes a simple peer-to-peer protocol based on BitTorrent. The model comprises a set of clients trying to download a file that has been partitioned into K blocks. Initially, there is one client that has already obtained all of the blocks and N additional clients with no blocks. Each client can download a block from any of the others but they can only attempt four concurrent downloads for each block.

Our model is represented as a CTMC. The PRISM source code for this case study (when N=4 and K=5) is given below.

// Simple peer-to-peer file distribution protocol based on BitTorrent
// gxn/dxp Jan 2006

ctmc

// N=4 clients, K=5 blocks to be downloaded
// Actually there are N+1=5 clients, one of which has all blocks initially

// Rate of block download for a single source
const double mu=2;

// Rate of download of block i:
// A client can download from the single client which starts with all blocks
// or from anyone that has subsequently downloaded it.
// Total number of concurrent downloads for each block is 4.
formula rate1=mu*(1+min(3,b11+b21+b31+b41));
formula rate2=mu*(1+min(3,b12+b22+b32+b42));
formula rate3=mu*(1+min(3,b13+b23+b33+b43));
formula rate4=mu*(1+min(3,b14+b24+b34+b44));
formula rate5=mu*(1+min(3,b15+b25+b35+b45));

// client 1
module client1
	
	// bij - has client i downloaded block j yet?
	b11 : [0..1];
	b12 : [0..1];
	b13 : [0..1];
	b14 : [0..1];
	b15 : [0..1];
	
	// Downloading of each block (see rate computations above)
	[] b11=0 -> rate1 : (b11'=1);
	[] b12=0 -> rate2 : (b12'=1);
	[] b13=0 -> rate3 : (b13'=1);
	[] b14=0 -> rate4 : (b14'=1);
	[] b15=0 -> rate5 : (b15'=1);
	
endmodule

// construct remaining clients through renaming
module client2=client1[b11=b21,b12=b22,b13=b23,b14=b24,b15=b25,b21=b11,b22=b12,b23=b13,b24=b14,b25=b15] endmodule
module client3=client1[b11=b31,b12=b32,b13=b33,b14=b34,b15=b35,b31=b11,b32=b12,b33=b13,b34=b14,b35=b15] endmodule
module client4=client1[b11=b41,b12=b42,b13=b43,b14=b44,b15=b45,b41=b11,b42=b12,b43=b13,b44=b14,b45=b15] endmodule

// labels
label "done1" = b11+b12+b13+b14+b15 = 5; // client 1 has received all blocks
label "done2" = b21+b22+b23+b24+b25 = 5; // client 2 has received all blocks
label "done3" = b31+b32+b33+b34+b35 = 5; // client 3 has received all blocks
label "done4" = b41+b42+b43+b44+b45 = 5; // client 4 has received all blocks
label "done" = (b11+b12+b13+b14+b15)+(b21+b22+b23+b24+b25)+(b31+b32+b33+b34+b35)+(b41+b42+b43+b44+b45) = 20; // all clients have received all blocks

// reward: fraction of blocks received
rewards "frac_rec"
	true : ((b11+b12+b13+b14+b15)/5)/4;
	true : ((b21+b22+b23+b24+b25)/5)/4;
	true : ((b31+b32+b33+b34+b35)/5)/4;
	true : ((b41+b42+b43+b44+b45)/5)/4;
endrewards
View: printable version          Download: peer2peer4_5.sm

Model Statistics

The table below gives information about the CTMC representing the model: the number of states and the number of transitions.

N: K: Model:
States: Transitions:
4 465,536 524,288
51,048,576 10,485,760
616,777,216 201,326,592
7268,435,456 3,758,096,384
84,294,967,29668,719,476,736
5 41,048,576 10,485,760
533,554,432 419,430,400
61,073,741,824 16,106,127,360
734,359,738,368601,295,421,440

Model Construction Times

The table below gives the times taken to construct the models. This process involves first building a CTMC (represented as an MTBDD) from the system description (in our module based language), and then computing the reachable states using a BDD based fixpoint algorithm. The total time required and the number of fixpoint iterations are given below.

N: K: Model:
Time (s): Iter.s:
4 4170.00
5210.01
6250.01
7290.02
8330.02
5 4210.00
5260.01
6310.02
7360.03

Model Checking

We have model checked the following property:

  • "the probability that all clients have received all blocks by time T"

The corresponding CSL formula is given by:

const double T; // time bound

// probability that all clients have received all blocks by time T
P=? [ true U<=T  "done"  ]

// expected fraction of blocks received by time T
R=? [ I=T ]

View: printable version          Download: peer2peer.csl

In the graphs below we have plotted these probabilities from a range of values of T.

  • N=4 (full time range) plot: graph for N=4 and K=4,5,...,8
  • N=4 (zoom) plot: graph for N=4 and K=4,5,...,8 (zoom)
  • N=5 (full time range) plot: graph for N=5 and K=4,5,...,7
  • N=5 (zoom) plot: graph for N=5 and K=4,5,...,7 (zoom)

Case Studies