Huang Lei, Jiaming Guo, Guanhua He, Xishan Zhang, Rui Zhang, Shaohui Peng, Shaoli Liu, Tianshi Chen. Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). 2024.

Hyper-parameter tuning (HPT) for deep learning (DL) models is prohibitively expensive. Sequential model-based optimization (SMBO) emerges as the state-of-the-art (SOTA) approach to automatically optimize HPT performance due to its heuristic advantages. Unfortunately, focusing on algorithm optimization rather than a large-scale parallel HPT system, existing SMBO-based approaches still cannot effectively remove their strong sequential nature, posing two performance problems: (1)extremely low tuning speedand (2)sub-optimal model quality. In this paper, we propose FastTuning, a fast, scalable, and generic system aiming at parallelly accelerating SMBO-based HPT for large DL/ML models. The key is to partition the highly complex search space into multiple smaller sub-spaces, each of which is assigned to and optimized by a different tuning worker in parallel. However, determining the right level of resource allocation to strike a balance between quality and cost remains a challenge. To address this, we further propose NIMBLE, a dynamic scheduling strategy that is specially designed for FastTuning, including (1) Dynamic Elimination Algorithm, (2) Sub-space Re-division, and (3) Posterior Information Sharing. Finally, we incorporate 6 SOTAs (i.e., 3 tuning algorithms and 3 parallel tuning tools) into FastTuning. Experimental results, on ResNet18, VGG19, ResNet50, and ResNet152, show that FastTuning can consistently offer much faster tuning speed (up to$80\times$) with better accuracy (up to 4.7% improvement), thereby enabling the application of automatic HPT to real-life DL models.

Giotto is a time-triggered embedded programming language which provides an abstract programming model for hard real-time applications. It effectively decouples the implementation from the design. A Giotto program focuses on the functionality and timing of periodic tasks. All the actions, e.g., task invocations, actuator updates, and mode switches, described in Giotto programs are triggered by real time. We take the views of the concerns of Giotto programs, including the reaction to the environment, the communication between tasks, the timing predictability, etc. Our goal is to simulate Giotto programs using a timed CSP-based model which can effectively express the concerns and can be used to verify safety properties. This paper is a first step that presents the timed CSP model for Giotto programs. We also give a case study to illustrate the utility of the timed CSP model. Based on the existing research for CSP with time, we believe that our model can support to analyze and verify safety properties of Giotto programs.

Automated verification of operating system kernels is a challenging problem, partly due to the use of shared mutable data structures. In this paper, we show how we can automatically verify memory safety and functional correctness of the task scheduler component of the FreeRTOS kernel using the verification system HIP/SLEEK. We show how some of HIP/SLEEK features like user-defined predicates and lemmas make the specifications highly expressive and the verification process viable. To the best of our knowledge, this is the first code-level verification of memory safety and functional correctness properties of the FreeRTOS scheduler. The outcome of our experiment confirms that HIP/SLEEK can indeed be used to verify code that is used in production. Moreover, since the properties that we verify are quite general, we envisage that the same approach can be adopted to verify the scheduler of other operating systems.

Memory is a constrained resource for software, and memory consumption is an essential factor to evaluate a program's performance. Therefore, there are existing works which concentrated on the inference of programs' memory usage. However, previous works mainly exploited type systems to infer programs' memory consumption, which were weak at handling aliasing information for heap manipulating programs. In this work, we propose an automated inference system for programs' memory usage based on the framework of Nguyen et al. The system can capture both the maximum requirement and the net usage of memory. We employ a separation logic based forward analysis to track the program's execution symbolically, and use symbolic Presburger arithmetic expressions to express the effect of allocation and deallocation in heap memory. Our approach is sound, and is also expected to provide more precision and scalability than previous works.

Memory usage analysis is an important problem for resource-constrained mobile devices, especially under mission- or safety-critical circumstances. Program codes running on or being downloaded into such devices are often available in low-level bytecode forms. We propose in this paper a formal heap model for Java bytecode language, on top of which we can then provide separation logic support for further memory usage verification. Our low-level heap model for Java bytecode would allow us to reason about the size and alignment properties of primitive values stored in the heap. To support type-related reasoning such as guaranteeing type and alignment safety, this model is also lifted with both base types and user-defined classes. Based on such model, we have also defined a separation logic proof system whose assertions are interpreted using the lifted heap with types. We envision, with further extension, the system would provide good support for memory usage analysis and verification for mobile devices.

Formal specifications have been a focus of software engineering research for many years and have been applied in a wide variety of settings. Their use in software engineering not only promotes high-level verification via theorem proving or model checking, but also inspires the "correct-by- construction" approach to software development via formal refinement. Although this correct-by-construction method proves to work well for small software systems, it is still a Utopia in the development of large and complex software systems. This paper moves one step forward in this direction by designing and implementing a sound linkage between the high level specification language Object-Z and the object-oriented specification language Spec#. Such a linkage would allow system requirements to be specified in a high-level formal language but validated and used in program language level. This linking process can be readily integrated with an automated program refinement procedure to achieve correctness-by-construction. In case no such procedures are applicable, the obtained contract- based specification can guide programmers to manually generate program code, which can then be verified against the obtained specification using any available program verifiers.