We present the verification of the machine-level implementation of a conservative variant of the standard mark-sweep garbage collector in a Hoare-style program logic. The specification of the collector is given on a m...We present the verification of the machine-level implementation of a conservative variant of the standard mark-sweep garbage collector in a Hoare-style program logic. The specification of the collector is given on a machine-level memory model using separation logic, and is strong enough to preserve the safety property of any common mutator program. Our verification is fully implemented in the Coq proof assistant and can be packed immediately as foundational proof-carrying code package. Our work makes important attempt toward building fully certified production-quality garbage collectors.展开更多
In the previous work of garbage collection （GC） models, scheduling analysis was given based on an assumption that there were no aperiodic mutator tasks. However, it is not true in practical real-time systems. The GC...In the previous work of garbage collection （GC） models, scheduling analysis was given based on an assumption that there were no aperiodic mutator tasks. However, it is not true in practical real-time systems. The GC algorithm which can schedule aperiodic tasks is proposed, and the variance of live memory is analyzed. In this algorithm, active tasks are deferred to be processed by GC until the states of tasks become inactive, and the saved sporadic server time can be used to schedule aperiodic tasks. Scheduling the sample task sets demonstrates that this algorithm in this paper can schedule aperiodic tasks and decrease GC work. Thus, the GC algorithm proposed is more flexible and portable.展开更多
基金Supported by the National Natural Science Foundation of China under Grant No.60673126(Verification and Compilation of Software Safety)Intel China Research Center.
文摘We present the verification of the machine-level implementation of a conservative variant of the standard mark-sweep garbage collector in a Hoare-style program logic. The specification of the collector is given on a machine-level memory model using separation logic, and is strong enough to preserve the safety property of any common mutator program. Our verification is fully implemented in the Coq proof assistant and can be packed immediately as foundational proof-carrying code package. Our work makes important attempt toward building fully certified production-quality garbage collectors.
基金supported by the 863 Program under Grant No2007AA01Z131
文摘In the previous work of garbage collection （GC） models, scheduling analysis was given based on an assumption that there were no aperiodic mutator tasks. However, it is not true in practical real-time systems. The GC algorithm which can schedule aperiodic tasks is proposed, and the variance of live memory is analyzed. In this algorithm, active tasks are deferred to be processed by GC until the states of tasks become inactive, and the saved sporadic server time can be used to schedule aperiodic tasks. Scheduling the sample task sets demonstrates that this algorithm in this paper can schedule aperiodic tasks and decrease GC work. Thus, the GC algorithm proposed is more flexible and portable.
