Resource-Tracking Concurrent Games
Résumé
We present a framework for game semantics based on concurrent
games, that keeps track of resources as data modified throughout
execution but not affecting its control flow. Our leading example
is time, yet the construction is in fact parametrized by a
resource bimonoid R, an algebraic structure expressing resources
and the effect of their consumption either sequentially or in
parallel. Relying on our construction, we give a sound
resource-sensitive denotation to R-IPA, an affine higher-order
concurrent programming language with shared state and a primitive
for resource consumption in R. Compared with general operational
semantics parametrized by R, our resource analysis turns out to
be finer, leading to non-adequacy. Yet, our model is not
degenerate as adequacy holds for an operational semantics
specialized to time.
In regard to earlier semantic frameworks for tracking resources,
the main novelty of our work is that it is based on a
non-interleaving semantics, and as such accounts for parallel use
of resources accurately.