The fast acceptance of cloud technology to industry explains increasing energy conservation needs and adoption of energy aware scheduling methods to cloud. Power consumption is one of the top of mind issues in cloud, ...The fast acceptance of cloud technology to industry explains increasing energy conservation needs and adoption of energy aware scheduling methods to cloud. Power consumption is one of the top of mind issues in cloud, because the usage of cloud storage by the individuals or organization grows rapidly. Developing an efficient power management processor architecture has gained considerable attention. However, the conventional power management mechanism fails to consider task scheduling policies. Therefore, this work presents a novel energy aware framework for power management. The proposed system leads to the development of Inclusive Power-Cognizant Processor Controller (IPCPC) for efficient power utilization. To evaluate the performance of the proposed method, simulation experiments inputting random tasks as well as tasks collected from Google Trace Logs were conducted to validate the supremacy of IPCPC. The research based on Real world Google Trace Logs gives results that proposed framework leads to less than 9% of total power consumption per task of server which proves reduction in the overall power needed.展开更多
Architectures based on the data flow computing model provide an alternative to the conventional Von-Neumann architecture that are widelyused for general purpose computing.Processors based on the data flow architecture...Architectures based on the data flow computing model provide an alternative to the conventional Von-Neumann architecture that are widelyused for general purpose computing.Processors based on the data flow architecture employ fine-grain data-driven parallelism.These architectures have thepotential to exploit the inherent parallelism in compute intensive applicationslike signal processing,image and video processing and so on and can thusachieve faster throughputs and higher power efficiency.In this paper,severaldata flow computing architectures are explored,and their main architecturalfeatures are studied.Furthermore,a classification of the processors is presented based on whether they employ either the data flow execution modelexclusively or in combination with the control flow model and are accordinglygrouped as exclusive data flow or hybrid architectures.The hybrid categoryis further subdivided as conjoint or accelerator-style architectures dependingon how they deploy and separate the data flow and control flow executionmodel within their execution blocks.Lastly,a brief comparison and discussionof their advantages and drawbacks is also considered.From this study weconclude that although the data flow architectures are seen to have maturedsignificantly,issues like data-structure handling and lack of efficient placementand scheduling algorithms have prevented these from becoming commerciallyviable.展开更多
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...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.展开更多
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 pap...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.展开更多
文摘The fast acceptance of cloud technology to industry explains increasing energy conservation needs and adoption of energy aware scheduling methods to cloud. Power consumption is one of the top of mind issues in cloud, because the usage of cloud storage by the individuals or organization grows rapidly. Developing an efficient power management processor architecture has gained considerable attention. However, the conventional power management mechanism fails to consider task scheduling policies. Therefore, this work presents a novel energy aware framework for power management. The proposed system leads to the development of Inclusive Power-Cognizant Processor Controller (IPCPC) for efficient power utilization. To evaluate the performance of the proposed method, simulation experiments inputting random tasks as well as tasks collected from Google Trace Logs were conducted to validate the supremacy of IPCPC. The research based on Real world Google Trace Logs gives results that proposed framework leads to less than 9% of total power consumption per task of server which proves reduction in the overall power needed.
文摘Architectures based on the data flow computing model provide an alternative to the conventional Von-Neumann architecture that are widelyused for general purpose computing.Processors based on the data flow architecture employ fine-grain data-driven parallelism.These architectures have thepotential to exploit the inherent parallelism in compute intensive applicationslike signal processing,image and video processing and so on and can thusachieve faster throughputs and higher power efficiency.In this paper,severaldata flow computing architectures are explored,and their main architecturalfeatures are studied.Furthermore,a classification of the processors is presented based on whether they employ either the data flow execution modelexclusively or in combination with the control flow model and are accordinglygrouped as exclusive data flow or hybrid architectures.The hybrid categoryis further subdivided as conjoint or accelerator-style architectures dependingon how they deploy and separate the data flow and control flow executionmodel within their execution blocks.Lastly,a brief comparison and discussionof their advantages and drawbacks is also considered.From this study weconclude that although the data flow architectures are seen to have maturedsignificantly,issues like data-structure handling and lack of efficient placementand scheduling algorithms have prevented these from becoming commerciallyviable.
基金supported by the National Natural Science Foundation of China under Grant Nos.61632005 and 62032004.
文摘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.
基金This work was supported by the National Natural Science Foundation of China under Grant No.61632005.
文摘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.