A method for automatic verification of cache coherence protocols is presented, in which cache coherence protocols are modeled as concurrent value-passing processes, and control and data consistency requirement are des...A method for automatic verification of cache coherence protocols is presented, in which cache coherence protocols are modeled as concurrent value-passing processes, and control and data consistency requirement are described as formulas in first-order p-calculus. A model checker is employed to check if the protocol under investigation satisfies the required properties. Using this method a data consistency error has been revealed in a well-known cache coherence protocol. The error has been corrected, and the revised protocol has been shown free from data consistency error for any data domain size, by appealing to data independence technique.展开更多
Inference systems for observation equivalences in the pi-calculus with recursion are proposed, and their completeness over the finite-control fragment with guarded recursions are proven. The inference systems consist ...Inference systems for observation equivalences in the pi-calculus with recursion are proposed, and their completeness over the finite-control fragment with guarded recursions are proven. The inference systems consist of inference rules and equational axioms. The judgments are conditional equations which characterise symbolic bisimulations between process terms. This result on the one hand generalises Milner’s complete axiomatisation of observation equivalence for regular CCS to the pi-calculus, and on the other hand extends the proof systems of strong bisimulations for guarded regular pi-calculus to observation equivalences.展开更多
A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown...A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown that the satisfiability of the two-variable sub-logic HML(FO2) of HML(FO) is decidable, and the complexity discussed. Finally, a decision procedure for model checking the value-passing processes with respect to HML(FO2) is obtained.展开更多
Current multi-operator image resizing methods succeed in generating impressive results by using image similarity measure to guide the resizing process. An optimal operation path is found in the resizing space. However...Current multi-operator image resizing methods succeed in generating impressive results by using image similarity measure to guide the resizing process. An optimal operation path is found in the resizing space. However, their slow resizing speed caused by inefficient computation strategy of the bidirectional patch matching becomes a drawback in practical use. In this paper, we present a novel method to address this problem. By combining seam carving with scaling and cropping, our method can realize content-aware image resizing very fast. We define cost functions combing image energy and dominant color descriptor for all the operators to evaluate the damage to both local image content and global visual effect. Therefore our algorithm can automatically find an optimal sequence of operations to resize the image by using dynamic programming or greedy algorithm. We also extend our algorithm to indirect image resizing which can protect the aspect ratio of the dominant object in an image.展开更多
Simulation and visualization of aeolian sand movement and sand ripple evolution are a challenging subject. In this paper, we propose a physically based modeling and simulating method that can be used to synthesize san...Simulation and visualization of aeolian sand movement and sand ripple evolution are a challenging subject. In this paper, we propose a physically based modeling and simulating method that can be used to synthesize sandy terrain in various patterns. Our method is based on the mechanical behavior of individual sand grains, which are widely studied in the physics of blown sand. We accounted significant mechanisms of sand transportation into the sand model, such as saltation, successive saltation and collapsing, while simplified the vegetation model and wind field model to make the simulation feasible and affordable. We implemented the proposed method on the programming graphics processing unit （GPU） to get real-time simulation and rendering. Finally, we proved that our method can reflect many characteristics of sand ripple evolution through several demonstrations. We also gave several synthesized desert scenes made from the simulated height field to display its significance on application.展开更多
基金Supported by the Intel Strategic CAD Labs, the National Natural Science Foundation of China （Grant No. 60421001）, and the Chinese Academy of Sciences.
文摘A method for automatic verification of cache coherence protocols is presented, in which cache coherence protocols are modeled as concurrent value-passing processes, and control and data consistency requirement are described as formulas in first-order p-calculus. A model checker is employed to check if the protocol under investigation satisfies the required properties. Using this method a data consistency error has been revealed in a well-known cache coherence protocol. The error has been corrected, and the revised protocol has been shown free from data consistency error for any data domain size, by appealing to data independence technique.
基金Project supported by the National Natural Science Foundation of China (Grant No. 69683003) and the Chinese Academy of Sciences.
文摘Inference systems for observation equivalences in the pi-calculus with recursion are proposed, and their completeness over the finite-control fragment with guarded recursions are proven. The inference systems consist of inference rules and equational axioms. The judgments are conditional equations which characterise symbolic bisimulations between process terms. This result on the one hand generalises Milner’s complete axiomatisation of observation equivalence for regular CCS to the pi-calculus, and on the other hand extends the proof systems of strong bisimulations for guarded regular pi-calculus to observation equivalences.
基金This work was partially supported by the National Natural Science Foundationof China (Grant No. 69833020) the National High Technology Development Program of China (Grant No. 2002AA144050)the National Grand Fundamental Research 973 Program of China
文摘A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown that the satisfiability of the two-variable sub-logic HML(FO2) of HML(FO) is decidable, and the complexity discussed. Finally, a decision procedure for model checking the value-passing processes with respect to HML(FO2) is obtained.
基金supported by the National Natural Science Foundation of China (NSFC) under Grant Nos. 60872120, 60902078, 61172104the Natural Science Foundation of Beijing under Grant No. 4112061+2 种基金the Scientific Research Foundation for the Returned Overseas Chinese Scholars of State Education Ministry of Chinathe French System@tic Paris-Region (CSDL Project)the National Agency for Research of French (ANR)-NSFC under Grant No. 60911130368
文摘Current multi-operator image resizing methods succeed in generating impressive results by using image similarity measure to guide the resizing process. An optimal operation path is found in the resizing space. However, their slow resizing speed caused by inefficient computation strategy of the bidirectional patch matching becomes a drawback in practical use. In this paper, we present a novel method to address this problem. By combining seam carving with scaling and cropping, our method can realize content-aware image resizing very fast. We define cost functions combing image energy and dominant color descriptor for all the operators to evaluate the damage to both local image content and global visual effect. Therefore our algorithm can automatically find an optimal sequence of operations to resize the image by using dynamic programming or greedy algorithm. We also extend our algorithm to indirect image resizing which can protect the aspect ratio of the dominant object in an image.
基金supported in part by the National High Technology Research and Development 863 Program of China under Grant No. 2006AA01Z301the International Cooperation Project of Ministry of Science and Technology of China under Grant No. 2007DFC10740
文摘Simulation and visualization of aeolian sand movement and sand ripple evolution are a challenging subject. In this paper, we propose a physically based modeling and simulating method that can be used to synthesize sandy terrain in various patterns. Our method is based on the mechanical behavior of individual sand grains, which are widely studied in the physics of blown sand. We accounted significant mechanisms of sand transportation into the sand model, such as saltation, successive saltation and collapsing, while simplified the vegetation model and wind field model to make the simulation feasible and affordable. We implemented the proposed method on the programming graphics processing unit （GPU） to get real-time simulation and rendering. Finally, we proved that our method can reflect many characteristics of sand ripple evolution through several demonstrations. We also gave several synthesized desert scenes made from the simulated height field to display its significance on application.
