TY - JOUR

T1 - A separation logic for negative dependence

AU - Bao, Jialu

AU - Gaboardi, Marco

AU - Hsu, Justin

AU - Tassarotti, Joseph

N1 - Funding Information:
We thank the anonymous reviewers for their helpful feedback and suggestions. This work benefited from discussions with Simon Docherty. This work was supported in part by the NSF under Grant No. 2035314, 1943130, 2040249, 2040222 and 2152831.
Publisher Copyright:
© 2022 Owner/Author.

PY - 2022/1

Y1 - 2022/1

N2 - Formal reasoning about hashing-based probabilistic data structures often requires reasoning about random variables where when one variable gets larger (such as the number of elements hashed into one bucket), the others tend to be smaller (like the number of elements hashed into the other buckets). This is an example of negative dependence, a generalization of probabilistic independence that has recently found interesting applications in algorithm design and machine learning. Despite the usefulness of negative dependence for the analyses of probabilistic data structures, existing verification methods cannot establish this property for randomized programs. To fill this gap, we design LINA, a probabilistic separation logic for reasoning about negative dependence. Following recent works on probabilistic separation logic using separating conjunction to reason about the probabilistic independence of random variables, we use separating conjunction to reason about negative dependence. Our assertion logic features two separating conjunctions, one for independence and one for negative dependence. We generalize the logic of bunched implications (BI) to support multiple separating conjunctions, and provide a sound and complete proof system. Notably, the semantics for separating conjunction relies on a non-deterministic, rather than partial, operation for combining resources. By drawing on closure properties for negative dependence, our program logic supports a Frame-like rule for negative dependence and monotone operations. We demonstrate how LINA can verify probabilistic properties of hash-based data structures and balls-into-bins processes.

AB - Formal reasoning about hashing-based probabilistic data structures often requires reasoning about random variables where when one variable gets larger (such as the number of elements hashed into one bucket), the others tend to be smaller (like the number of elements hashed into the other buckets). This is an example of negative dependence, a generalization of probabilistic independence that has recently found interesting applications in algorithm design and machine learning. Despite the usefulness of negative dependence for the analyses of probabilistic data structures, existing verification methods cannot establish this property for randomized programs. To fill this gap, we design LINA, a probabilistic separation logic for reasoning about negative dependence. Following recent works on probabilistic separation logic using separating conjunction to reason about the probabilistic independence of random variables, we use separating conjunction to reason about negative dependence. Our assertion logic features two separating conjunctions, one for independence and one for negative dependence. We generalize the logic of bunched implications (BI) to support multiple separating conjunctions, and provide a sound and complete proof system. Notably, the semantics for separating conjunction relies on a non-deterministic, rather than partial, operation for combining resources. By drawing on closure properties for negative dependence, our program logic supports a Frame-like rule for negative dependence and monotone operations. We demonstrate how LINA can verify probabilistic properties of hash-based data structures and balls-into-bins processes.

KW - Probabilistic programs

KW - negative dependence

KW - separation logic

UR - http://www.scopus.com/inward/record.url?scp=85123210615&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85123210615&partnerID=8YFLogxK

U2 - 10.1145/3498719

DO - 10.1145/3498719

M3 - Article

AN - SCOPUS:85123210615

SN - 2475-1421

VL - 6

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - POPL

M1 - 3498696

ER -