{"id":"W3211705538","doi":"10.1145/3477082","title":"TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs","year":2021,"lang":"en","type":"article","venue":"ACM Transactions on Programming Languages and Systems","topic":"Distributed systems and fault tolerance","field":"Computer Science","cited_by":11,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"Horizon 2020; Engineering and Physical Sciences Research Council; European Commission; UK Research and Innovation","keywords":"Liveness; Computer science; Blocking (statistics); Correctness; Separation logic; Abstraction; Programming language; Implementation; Mutual exclusion; Concurrency; Theoretical computer science; Model checking; Distributed computing","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0002639228,0.0001438194,0.0002610076,0.00005810983,0.0001929366,0.0002542898,0.0002493289,0.00007428743,0.000002606911],"category_scores_gemma":[0.00003465631,0.0001314583,0.0001079706,0.0002419681,0.00004222218,0.0001836291,0.0000119713,0.00009425705,0.000001267625],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00002716639,"about_ca_system_score_gemma":0.00005112362,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0000963624,"about_ca_topic_score_gemma":0.00003814367,"domain_scores_codex":[0.9987695,0.00007317997,0.0003512401,0.0003432251,0.0002397177,0.0002231774],"domain_scores_gemma":[0.9989791,0.0001462498,0.0001560241,0.0003665506,0.0002756396,0.00007647145],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00001245117,0.0003635502,0.0001446398,0.0005214451,0.00009221595,0.00002337048,0.001269479,0.0002206096,0.001634963,0.01475442,0.00006093094,0.9809019],"study_design_scores_gemma":[0.01817555,0.006576091,0.006024929,0.01289288,0.0006477548,0.003058357,0.03068784,0.6343908,0.03547736,0.001214645,0.2463294,0.004524495],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.01839176,0.001890829,0.9779801,0.0003027585,0.0004906082,0.00067138,0.00009640895,0.0001246416,0.00005146854],"genre_scores_gemma":[0.9597558,0.00001354432,0.039468,0.00001387802,0.00005225908,0.0002993902,0.0001132247,0.000009864356,0.0002739842],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.9763774,"threshold_uncertainty_score":0.5360715,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01933573393885135,"score_gpt":0.2976680095504109,"score_spread":0.2783322756115595,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}