Lilo : Une logique de séparation concurrente relationnelle d'ordre supérieur pour la vivacité

La logique de séparation concurrente (CSL) a excellé dans la vérification des propriétés de sécurité dans diverses applications, mais son application aux propriétés de vivacité reste limitée. Bien que les approches existantes comme TaDA Live et les Sémantiques Opérationnelles Justes (FOS) aient fait des progrès significatifs, elles sont encore confrontées à des limites. TaDA Live a des difficultés à vérifier certaines classes de programmes, en particulier les objets concurrents avec des points de linéarisation non locaux, et manque de support pour les propriétés de vivacité générales telles que "de bonnes choses se produisent infiniment souvent". D'autre part, l'évolutivité de FOS est entravée par l'absence de principes de raisonnement modulaire sur les threads et de spécifications modulaires. Cet article introduit Lilo, une CSL relationnelle d'ordre supérieur conçue pour surmonter ces limitations. Notre observation centrale est que FOS nous aide à maintenir des primitives simples pour notre logique, ce qui nous permet d'explorer l'espace de conception avec moins de restrictions. En conséquence, Lilo adapte diverses techniques réussies de la littérature. Elle supporte le raisonnement sur des programmes non-terminants en soutenant les preuves de raffinement, et fournit également des invariants de style Iris et des spécifications modulaires pour faciliter la verification modulaire. Pour supporter le raisonnement d'ordre supérieur sans s'appuyer sur l'indexation par étapes, nous développons une technique appelée propositions stratifiées inspirées de Nola. En particulier, nous développons de nouvelles abstractions pour le raisonnement sur la vivacité qui rassemblent ces techniques de manière uniforme. Nous montrons l'évolutivité de Lilo à travers des études de cas, y compris la première vérification modulaire garantissant la terminaison de la pile d'élimination. Lilo et les exemples de cet article sont mécanisés dans Coq.