Circuit quantum electrodynamics with a quadruple quantum dot

In this theoretical work,we describe a mechanism for the coupling between a plane structure consisting of four quantum dots and a resonator.We systematically study the dependence of the quadruple coupling strength and the qubit decoherence rate and point out the optimized operating position of the hybrid system.According to the transmission given by the input-output theory,the signatures in the resonator spectrum are predicted.Furthermore,based on the parameters already achieved in previous works,we prove that the device described in this paper can achieve the strong coupling limit,i.e.,this approach can be used for system extension under the existing technical conditions.Our results show an effective and promotable approach to couple quantum dot structures in plane with the resonator and propose a meaningful extension method.

A parallel and scalable digital architecture for training support vector machines

To facilitate the application of support vector machines (SVMs) in embedded systems,we propose and test a parallel and scalable digital architecture based on the sequential minimal optimization (SMO) algorithm for training SVMs.By taking advantage of the mature and popular SMO algorithm,the numerical instability issues that may exist in traditional numerical algorithms are avoided.The error cache updating task,which dominates the computation time of the algorithm,is mapped into multiple processing units working in parallel.Experiment results show that using the proposed architecture,SVM training problems can be solved effectively with inexpensive fixed-point arithmetic and good scalability can be achieved.This architecture overcomes the drawbacks of the previously proposed SVM hardware that lacks the necessary flexibility for embedded applications,and thus is more suitable for embedded use,where scalability is an important concern.

Verification of Real Time Operating System Exception Management Based on SPARCv8

Exception management,as the lowest level function module of the operating system,is responsible for making abrupt changes in the control flow to react to exception events in the system.The correctness of the exception management is crucial to guaranteeing the safety of the whole system.However,existing formal verification projects have not fully considered the issues of exceptions at the assembly level.Especially for real-time operating systems,in addition to basic exception handling,there are nested exceptions and task switching by exceptions service routine.In our previous work,we used high-level abstraction to describe the basic elements of the exception management and verified correctness only at the requirement layer.Building on earlier work,this paper proposes EMS(Exception Management SPARCv8),a practical Hoare-style program framework to verify the exception management based on SPARCv8(Scalable Processor Architecture Version 8)at the design layer.The framework describes the low-level details of the machine,such as registers and memory stack.It divides the execution logic of the exception management into six phases for comprehensive formal modeling.Taking the executing scenario of the real-time operating system SpaceOS on the Beidou-3 satellite as an example,we use the EMS framework to verify the exception management.All the formalization and proofs are implemented in the interactive theorem prover Coq.

Modular Verification of SPARCv8 Code

Inline assembly code is common in system software to interact with the underlying hardware platforms. The safety and correctness of the assembly code is crucial to guarantee the safety of the whole system. In this paper, we propose a practical Hoare-style program logic for verifying SPARC (Scalable Processor Architecture) assembly code. The logic supports modular reasoning about the main features of SPARCv8 ISA (instruction set architecture), including delayed control transfers, delayed writes to special registers, and register windows. It also supports relational reasoning for refinement verification. We have applied it to verify that there is a contextual refinement between a context switch routine in SPARCv8 and a switch primitive. The program logic and its soundness proof have been mechanized in Coq.