Relational geometry modelling execution of structured programs

We discuss some twists around Concurrent Kleene Algebra (CKA). First, a new model of CKA represents a trace of a concurrent program as a diagram in a two-dimensional non-metric finite geometry, namely, program actions by points, objects and threads by vertical lines, transactions by horizontal lines, communications and resource sharing by sloping lines. While we had already sketched this earlier, we fully formalise it here in terms of the algebra of binary relations. Second, we present a new definition technique for partial operators, namely an assume/claim style akin to rely/guarantee program specification. This admits a general refinement order with Top and Bottom as well as proofs of the CKA laws. Finally, we give a short perspective on the geometric representation of some standard concurrent programming concepts