Simuliris: a separation logic framework for verifying concurrent program optimizations

Today’s compilers employ a variety of non-trivial optimizations to achieve good performance. One key trick compilers use to justify transformations of concurrent programs is to assume that the source program has no data races : if it does, they cause the program to have undefined behavior (UB) and give the compiler free rein. However, verifying correctness of optimizations that exploit this assumption is a non-trivial problem. In particular, prior work either has not proven that such optimizations preserve program termination (particularly non-obvious when considering optimizations that move instructions out of loop bodies), or has treated all synchronization operations as external functions (losing the ability to reorder instructions around them). In this work we present Simuliris , the first simulation technique to establish termination preservation (under a fair scheduler) for a range of concurrent program transformations that exploit UB in the source language. Simuliris is based on the idea of using ownership to reason modularly about the assumptions the compiler makes about programs with well-defined behavior. This brings the benefits of concurrent separation logics to the space of verifying program transformations: we can combine powerful reasoning techniques such as framing and coinduction to perform thread-local proofs of non-trivial concurrent program optimizations. Simuliris is built on a (non-step-indexed) variant of the Coq-based Iris framework, and is thus not tied to a particular language. In addition to demonstrating the effectiveness of Simuliris on standard compiler optimizations involving data race UB, we also instantiate it with Jung et al.’s Stacked Borrows semantics for Rust and generalize their proofs of interesting type-based aliasing optimizations to account for concurrency.

The short-term bias in policy programs for small business: exploring discontinuation of a successful growth program

PurposeWhen a successful policy intervention for small firm growth is ending, a continuation decision may be relevant. However, immediately after program termination, solid analysis of the growth of the treated firms in comparison with similar firms cannot be produced, so decision makers rely on less valid data. Moreover, the decision process is challenging because many players, alternative programs, decision levels and financial sources tend to be part of the process. In such a complex and volatile policy environment, successful programs may well be discontinued despite a clear continuation need. The purpose of the paper is to explore this weakness.Design/methodology/approachThe paper identifies four fundamental principles that are conducive for a rational continuation choice: “additionality,” “substitution,” “need” and “success”. It argues that if these principles are fulfilled, the rational choice would be to continue the program. To demonstrate that this rational outcome does not always happen in practice, an extreme case fulfilling the four principles well was selected.FindingsThe program aimed to enhance growth in small firms through manager training. It encompassed about 700 growth-oriented small firms in three years and was comprehensively evaluated after program termination. This evaluation demonstrated a high success rate of the program in all respects, including in terms of achieved growth compared to a control group of similar firms.Originality/valueThis discontinuation case suggests that non-rational reasoning plays a significant role in contemporary complex and volatile policy environments, which again points to a need for reform in this policy area.

Decision Tree Learning in CEGIS-Based Termination Analysis

We present a novel decision tree-based synthesis algorithm of ranking functions for verifying program termination. Our algorithm is integrated into the workflow of CounterExample Guided Inductive Synthesis (CEGIS). CEGIS is an iterative learning model where, at each iteration, (1) a synthesizer synthesizes a candidate solution from the current examples, and (2) a validator accepts the candidate solution if it is correct, or rejects it providing counterexamples as part of the next examples. Our main novelty is in the design of a synthesizer: building on top of a usual decision tree learning algorithm, our algorithm detects cycles in a set of example transitions and uses them for refining decision trees. We have implemented the proposed method and obtained promising experimental results on existing benchmark sets of (non-)termination verification problems that require synthesis of piecewise-defined lexicographic affine ranking functions.

Weight Change During a Clinical Weight Management Program: An Observational Cohort Study

ABSTRACT Background: The objective of this analysis was to describe weight loss results at 12 months of a clinical weight management program in which patients selected their treatment preference. Methods: 3,007 patients (mean ± SD; age = 50 ± 12 years, body mass index = 42 ± 8 kg·m−2, 80% female, 51% black) enrolled in the program at Henry Ford Hospital self-selected a 1,200 to 2,000 kcals hypocaloric, 1,000 to 1,500 kcals low calorie, or 500 to 900 kcals very low calorie meal plan. Meal plans were instructed by a dietitian and the low calorie and very low calorie meal plans incorporated the use of commercial meal replacements. Regular biweekly appointments were conducted by a clinical exercise physiologist. Program termination was at the patient's discretion. Change in body weight was analyzed at 12 months by linear mixed modeling and using the baseline observation carried forward method with repeated measure analysis of variance. Results: Average program participation was 5 months. Based on an intent-to-treat linear mixed modeling, the very low calorie group had the greatest 12-month weight loss (−13.9 ± 1.0 kg), followed by the low calorie and hypocaloric groups (−9.5 ± 0.6 and −6.0 ± 0.4 kg, respectively; P < 0.05 for both low calorie and hypocaloric vs very low calorie plan). The baseline observation carried forward analysis also demonstrated significant weight loss in all groups at 12 months. Conclusion: In this real-world weight management program setting of patients who self-selected a meal plan and length of participation, both very low calorie and low calorie plans resulted in more weight loss at 12 months than the hypocaloric plan.

The Role of Mental Health Courts in Mitigating Family Violence

Mental health courts are one potential means to mitigate violence against family members by people with mental illness. This study identified the rate at which cases of family violence come before a mental health court and the success of defendants charged with assaulting family members. In a sample of 1,456 defendants eligible to participate in a mental health court, descriptive statistics were used to report rates of admission of defendants charged with assaulting family members and their characteristics; a static group design was used to compare post-program rearrests among defendants who assaulted family members who successfully completed the program, who did not complete the program, and who did not participate despite being eligible; and logistic regression was used to determine the effect of participation on rearrest when controlling for demographic and clinical factors. The study found that family violence occurred in 24.7% of admitted cases. Most eligible defendants who assaulted family members (75.8%) participated in the court program, and among those who did, 72.2% successfully completed the program. Defendants who assaulted family members and had a positive program termination had a much lower rate of rearrest post-program completion compared with those who did not complete the program or did not participate despite being eligible, a finding that held when controlling for other factors. This study suggests that mental health courts can be an effective option for mitigating family violence committed by people with mental illness.