Quote: in ESP, memory safety is a local property of each process; reference counting of link/unlink; communicates immutable, acyclic objects; easily verified by SPIN

Quotation Skeleton

ESP provides a novel explicit management scheme to … ESP is designed to make memory safety a … [the same effect as] deep copies of the objects are delivered … [p. 314] each process is responsible for managing its … ESP provides a reference counting interface to manage … [footnote, ESP "does not have circular data structures.] … ESP is designed so that [object] link and … each process, the SPIN verifier can be used … [p. 316] To verify the memory safety of the … [VMMC] firmware required 40 lines of test code. The entire state … It took 0.5 second to complete and required … all the memory safety bugs but also some … collection. … [Although not used to debug the VMMC firmware, the SPIN verifier located an earlier bug and several introduced bugs.]   Google-1   Google-2

Copyright clearance needed for quotation.

Related Topics

Topic: memory management by reference counting (22 items)
Topic: safe use of pointers (102 items)