order reduction
Recently Published Documents

Dynamic partial order reduction (DPOR) verifies concurrent programs by exploring all their interleavings up to some equivalence relation, such as the Mazurkiewicz trace equivalence. Doing so involves a complex trade-off between space and time. Existing DPOR algorithms are either exploration-optimal (i.e., explore exactly only interleaving per equivalence class) but may use exponential memory in the size of the program, or maintain polynomial memory consumption but potentially explore exponentially many redundant interleavings. In this paper, we show that it is possible to have the best of both worlds: exploring exactly one interleaving per equivalence class with linear memory consumption. Our algorithm, TruSt, formalized in Coq, is applicable not only to sequential consistency, but also to any weak memory model that satisfies a few basic assumptions, including TSO, PSO, and RC11. In addition, TruSt is embarrassingly parallelizable: its different exploration options have no shared state, and can therefore be explored completely in parallel. Consequently, TruSt outperforms the state-of-the-art in terms of memory and/or time.

Many solar panels for spacecrafts are deployed by Tape Spring Hinges (TSHs) which have changeable stiffness. The stiffness of TSH is small when panels are folded, and it becomes large quickly in its deployed status. Since the solar panel is a thin sheet, flexible deformation is easily generated by orbit maneuvers. The coupling effect between the nonlinear TSHs and the flexible panels generates obvious vibration which affects the operational stability of the satellite. To investigate this coupling effect, non-deformable, linear deformable and nonlinear deformable panels were modelled by rigid body, modal order reduction method (MORM) and finite element method (FEM), respectively. The driving torque of TSH was described as a function of the rotation angle and angular velocity. The nonlinear properties of the TSH were reflected by one angle-stiffness spline multiplied by one stiffness coefficient. Dynamic responses of a satellite in deployment and orbit steering were analyzed by numerical simulations. Analysis results indicate the local deformation of panels keeps the stiffness of the TSH within a large range which accelerates the orbit maneuvers. However, much vibration is generated by the coupling effect if the luck-up status is broken up. The coupling effect affects the sequence of deployment, overshoot phenomenon and acceleration magnitude of the panels. Although the MORM is more efficient than FEM in computation, we propose FEM is better suited in the design of TSH and in studying the precise control of spacecraft with flexible solar panels and TSHs.