jm + lint   5

"Understanding Real-World Concurrency Bugs in Go" (paper)
'Go advocates for the usage of message passing as the means of inter-thread communication and provides several new concurrency mechanisms and libraries to ease multi-threading programming. It is important to understand the implication of these new proposals and the comparison of message passing and shared memory synchronization in terms of program errors, or bugs. Unfortunately, as far as we know, there has been no study on Go’s concurrency bugs. In this paper, we perform the first systematic study on concurrency bugs in real Go programs. We studied six popular Go software including Docker, Kubernetes, and gRPC.

We analyzed 171 concurrency bugs in total, with more than half of them caused by non-traditional, Go-specific problems. Apart from root causes of these bugs, we also studied their fixes, performed experiments to reproduce them, and evaluated them with two publicly-available Go bug detectors.
Overall, our study provides a better understanding on Go’s concurrency models and can guide future researchers and practitioners in writing better, more reliable Go software and in developing debugging and diagnosis tools for Go.'

(via Bill de hOra)
via:dehora  golang  go  concurrency  bugs  lint  synchronization  threading  threads  bug-detection 
19 days ago by jm
Argon2 code audits - part one - Infer
A pretty viable way to run Facebook's Infer dataflow static analysis tool (which is otherwise quite a bear to run).
infer  facebook  java  clang  errors  static-analysis  lint  dataflow  docker 
february 2016 by jm
Facebook Infer
New static analysis goodnews, freshly open-sourced by Facebook:
Facebook Infer uses logic to do reasoning about a program's execution, but reasoning at this scale — for large applications built from millions of lines of source code — is hard. Theoretically, the number of possibilities that need to be checked is more than the number of estimated atoms in the observable universe. Furthermore, at Facebook our code is not a fixed artifact but an evolving system, updated frequently and concurrently by many developers. It is not unusual to see more than a thousand modifications to our mobile code submitted for review in a given day. The requirements on the program analyzer then become even more challenging because we expect a tool to report quickly on these code modifications — in the region of 10 minutes — to fit in with developers' workflow. Coping with this scale and velocity requires advanced mathematical techniques. Facebook Infer uses two such techniques: separation logic and bi-abduction.

Separation logic is a theory that allows Facebook Infer's analysis to reason about small, independent parts of the application storage, rather than having to consider the entirety of the memory potentially at every step. That would be a daunting task on modern processors with their large addressable virtual memories.

Bi-abduction is a logical inference technique that allows Facebook Infer to discover properties about the behavior of independent parts of the application code. By storing these properties between runs, Facebook Infer needs to analyze only the parts of the software that have changed, reusing the results of its previous analysis where it can.

By combining these approaches, our analyzer is able to find complex problems in modifications to an application built from millions of lines of code, in minutes.


(via Bryan O'Sullivan)
via:bos  infer  facebook  static-analysis  lint  code  java  ios  android  coding  bugs 
june 2015 by jm
ShellCheck
Static code analysis for shell scripts (via Tony Finch)
bash  cli  sh  linux  shell  coding  static-analysis  lint 
april 2015 by jm
google/error-prone
Nice looking static code validation tool for Java, from Google. I recognise a few of these errors ;)
google  static  code-validation  lint  testing  java  coding 
february 2015 by jm

Copy this bookmark:



description:


tags: