RustHorn: CHC-based Verification for Rust Programs

Reduction to satisfiability of constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. Current CHC-based methods, however, do not work very well for pointer-manipulating programs, especially those with dynamic memory allocation. This article presents a novel reduction of pointer-manipulating Rust programs into CHCs, which clears away pointers and memory states by leveraging Rust’s guarantees on permission. We formalize our reduction for a simplified core of Rust and prove its soundness and completeness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.

Adaptive Layered Segregated Fit Scheme for Dynamic Memory Allocation

Embedded applications are becoming more complex and are required to utilize computing platform resources more efficiently. Existing dynamic memory allocation (DSA) schemes cannot adaptively perform memory management according to the environment in which they are located or integrate various memory allocation strategies, making it impossible to guarantee a constant execution time. Efficient memory utilization is a crucial challenge for developers, especially in embedded OSs (operating systems). In this paper, we propose an adaptive layered segregated fit (ALSF) scheme for DSA. The ALSF scheme combines dynamic two-dimensional arrays and bitmaps, completes the allocation and freeing of memory blocks within constant execution time, and uses memory splitting technology to reduce internal fragmentation. The proposed scheme also adjusts the number of segregated lists by analyzing the system’s allocation of different memory sizes, which improves the matching accuracy of memory blocks. We conducted a comparative experimental analysis and investigation of the ALSF and two-level segregated fit (TLSF) schemes in the Zephyr OS. Experiments show that the average memory utilization of the proposed ALSF scheme reaches 94.95%. Compared with the TLSF scheme, our scheme has a 12.99% higher allocation success rate in the memory-scarce environment, and the execution speeds of the two are similar.

Scalable Codes for Precision Calculations of Properties of Complex Atomic Systems

High precision atomic data are indispensable for studies of fundamental symmetries, tests of fundamental physics postulates, developments of atomic clocks, ultracold atom experiments, astrophysics, plasma science, and many other fields of research. We have developed a new parallel atomic structure code package that enables computations that were not previously possible due to system complexity. This code package also allows much quicker computations to be run with higher accuracy for simple systems. We explored different methods of load-balancing matrix element calculations for many-electron systems, which are very difficult due to the intrinsic nature of the computational methods used to calculate them. Furthermore, dynamic memory allocation and MPI parallelization have been implemented to optimize and accelerate the computations. We have achieved near-perfect linear scalability and efficiency with the number of processors used for calculation, paving the way towards the future where most open-shell systems will finally be able to be treated with good accuracy. We present several examples illustrating new capabilities of the newly developed codes, specifically correlating up to all 60 electrons in the highly charged Ir17+ ion and predicting certain properties of Fe16+.

OTA Firmware Update for Texas Instruments C2000 Controllers

Firmware updates are necessary to enhance the embedded systems performance and to remove the bugs. But it’s not an efficient manner to be installed it by the technician in the field. For c2000 controllers of Texas instruments dynamic memory allocation is not possible. So, using the proposed method we can maintain both updated firmware and current running firmware for the continuity of the system operation without dynamic memory allocation requirement. In this over the air (OTA) firmware update method, both application and the secondary boot loader (SBL) handles the update process without intervention of the technician. When there is any update the current running application copies the incoming updated firmware using its linker file. After the update process when there is a system reset the SBL calculates the checksum of the updated application, if it matches with the received checksum it executes the updated firmware else it executes the current running firmware without interrupting the application operation.