Most logics for stateful reasoning in a concurrent setting are designed around a parallel composition operator ||. Given two programs p1 and p2, || composes them concurrently, creating a new program p1 || p2 where resources are shared amongst two threads, with p1 and p2 potentially racing for a shared resource. This syntactic, well-bracketed approach enables reasoning inductively and fosters modular reasoning, but it enforces a fixed synchronization pattern between the forked threads. On the other hand, in most real-world concurrent programming environments, threads are spawned dynamically using fork primitives. This practice allows for more flexible synchronization patterns between threads, but also hinders the modular verification of programs.

In this talk, we discuss an ongoing attempt to develop new logics for stateful reasoning in an unstructured concurrency setting. In particular, we propose a logic for fork/join concurrency that can reason modularly about forked threads and their interference. Our approach consists of bridging two previous works: we propose to combine the compositional expressiveness of fine-grained resources and FCSL with some lessons learnt while developing dependent type theories for stateful unstructured control.