Handling Large States

Protocol implementations can have large states. For the TCP model discussed in Section 3.3, each state is around $250$ kilobytes, which is shown in Table 1. Note that a process in the TCP model runs the entire Linux kernel. Thus, the process state consists of all the global variables in the kernel ($78$KB), and any memory dynamically allocated during the kernel boot-up and the subsequent processing of TCP events ($25$KB). Additionally, the process runs three kernel threads (§3.3), each of which run in a separate $8$KB stack. ² The system consists of two such processes along with a model of the network, resulting in a state that is $250$KB in size.