Advertisement

Experience Developing and Deploying Concurrency Analysis at Facebook

  • Peter O’Hearn
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11002)

Abstract

This paper tells the story of the development of RacerD, a static program analysis for detecting data races that is in production at Facebook. The technical details of RacerD are described in a separate paper; we concentrate here on how the project unfolded from a human point of view. The paper describes, in this specific case, the benefits of feedback between science and engineering, the tension encountered between principle and compromise, and how being flexible and adaptable in the presence of a changing engineering context can lead to surprising results which far exceed initial expectations. I hope to give the reader an impression of what it is like to develop advanced static analyses in industry, how it is both different from and similar to developing analyses for the purpose of advancing science.

Notes

Acknowledgements

Thanks first of all to Jingbo Yang and Ben Jaeger for being so giving of their time, experience and insight when working with Sam Blackshear and I. And thanks to Sam for taking the engineering of RacerD to another level. I am fortunate to have participated in this collaboration with Ben, Jingbo and Sam. I’m grateful to Nikos Gorogiannis and Ilya Sergey for joining and contributing greatly to the project. Finally, special thanks to Bryan O’Sullivan for consistently and enthusiastically supporting this work, and encouraging me to proceed and be bold.

References

  1. 1.
    Blackshear, S., Gorogiannis, N., Sergey, I., O’Hearn, P.: RacerD: compositional static race detection. In: OOPSLA (2018)Google Scholar
  2. 2.
    Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: 32nd POPL, pp. 59–70 (2005)Google Scholar
  3. 3.
    Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003).  https://doi.org/10.1007/3-540-44898-5_4CrossRefGoogle Scholar
  4. 4.
    Brookes, S., O’Hearn, P.W.: Concurrent separation logic. SIGLOG News 3(3), 47–65 (2016)Google Scholar
  5. 5.
    Calcagno, C., et al.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3–11. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-17524-9_1CrossRefGoogle Scholar
  6. 6.
    Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26 (2011)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Harman, M., O’Hearn, P.: From start-ups to scale-ups: open problems and challenges in static and dynamic program analysis for testing and verification (keynote paper). In: International Working Conference on Source Code Analysis and Manipulation (2018)Google Scholar
  8. 8.
    O’Hearn, P.: Continuous reasoning: scaling the impact of formal methods. In: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Oxford, July 2018Google Scholar
  9. 9.
    O’Hearn, P.W.: Resources, concurrency and local reasoning. Theor. Comput. Sci. 375(1–3), 271–307 (2007)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Tennent, R.D.: Language design methods based on semantic principles. Acta Inf. 8, 97–112 (1977)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Peter O’Hearn
    • 1
  1. 1.FacebookLondonUK

Personalised recommendations