The ISO C standard does not specify the semantics of many valid programs that use non-portable idioms such as integer-pointer casts. Recent efforts at formal definitions and verified implementation of the C language inherit this feature. By adopting high-level abstract memory models, they validate common optimizations. On the other hand, this prevents reasoning about much low-level code relying on the behavior of common implementations, where formal verification has many applications. We present the first formal memory model that allows many common optimizations and fully supports operations on the representation of pointers. All arithmetic operations are well-defined for pointers that have been cast to integers. Crucially, our model is also simple to understand and program with. All our results are fully formalized in Coq.

Interleaved Polling with Adaptive Cycle Time (IPACT) is one of the earliest proposed polling schemes for dynamic bandwidth allocation in Ethernet Passive Optical Networks (EPONs) and has been extensively used as a benchmark by many subsequent allocation schemes. In this paper, we attempt to construct a mathematical model of the IPACT scheme under the gated service discipline. For N = 1 ONU, we derive closed-form expression for the steady state grant size. For N > 1 ONUs, we need to consider separately a small and a large load-distance ratio. For the former case, the N = 1 ONU model holds even for N > 1. For the latter case, we find a closed form expression for the grant size. Our model shows a reasonable match with the values obtained from simulation for the steady state queue size and hence the throughput and delay.