This paper analyzes some problems of the current teaching situation in the course High-level Programming Language,such as the lagging content of the course compared with technology development,the emphasis on theory r...This paper analyzes some problems of the current teaching situation in the course High-level Programming Language,such as the lagging content of the course compared with technology development,the emphasis on theory rather than on practice,the low enthusiasm of students for learning,and the weak practical ability of students.In response to the needs of enterprises for talents under the background of New Engineering,especially the cultivation of students’adaptability and practical abilities towards future industries to improve students’knowledge and problemsolving abilities to keep up with the modern technology,this paper proposes the ways and methods to reform and explore the teaching content and teaching methods by integrating industry and education,assisting teaching according to industrial demands,and lowering technology barriers of new technology.The practical effect is evaluated through a survey in class and the follow-up questionnaire after class,and the results show that the effect of the practice is effective.展开更多
Network processors (NPs) are widely used for programmable and high-performance networks;however, the programs for NPs are less portable, the number of NP program developers is small, and the development cost is high. ...Network processors (NPs) are widely used for programmable and high-performance networks;however, the programs for NPs are less portable, the number of NP program developers is small, and the development cost is high. To solve these problems, this paper proposes an open, high-level, and portable programming language called “Phonepl”, which is independent from vendor-specific proprietary hardware and software but can be translated into an NP program with high performance especially in the memory use. A common NP hardware feature is that a whole packet is stored in DRAM, but the header is cached in SRAM. Phonepl has a hardware-independent abstraction of this feature so that it allows programmers mostly unconscious of this hardware feature. To implement the abstraction, four representations of packet data type that cover all the packet operations (including substring, concatenation, input, and output) are introduced. Phonepl have been implemented on Octeon NPs used in plug-ins for a network-virtualization environment called the VNode Infrastructure, and several packet-handling programs were evaluated. As for the evaluation result, the conversion throughput is close to the wire rate, i.e., 10 Gbps, and no packet loss (by cache miss) occurs when the packet size is 256 bytes or larger.展开更多
The Spatio-Temporal Consistency Language(STeC)is a high-level modeling language that deals natively with spatio-temporal behaviour,i.e.,behaviour relating to certain locations and time.Such restriction by both locatio...The Spatio-Temporal Consistency Language(STeC)is a high-level modeling language that deals natively with spatio-temporal behaviour,i.e.,behaviour relating to certain locations and time.Such restriction by both locations and time is of first importance for some types of real-time systems.CCSL is a formal specification language based on logical clocks.It is used to describe some crucial safety properties for real-time systems,due to its powerful expressiveness of logical and chronometric time constraints.We consider a novel verification framework combining STeC and CCSL,with the advantages of addressing spatio-temporal consistency of system behaviour and easily expressing some crucial time constraints.We propose a theory combining these two languages and a method verifying CCSL properties in STeC models.We adopt UPPAAL as the model checking tool and give a simple example to illustrate how to carry out verification in our framework.展开更多
A program construction method based on Gamma language is proposed. The problemto be solved is specified by first-order predicate logic and a semantic verification program isconstructed directly from the specification....A program construction method based on Gamma language is proposed. The problemto be solved is specified by first-order predicate logic and a semantic verification program isconstructed directly from the specification. Ways for improving efficiency of the program arealso studied. The method differs from the one proposed by Manna and Waldinger, where aprogram is extracted from the proof of the existence of an object meeting the given specification.On the other hand, it also differs from the classical one used for deriving Gamma programsof Banatre and Le Metayer, which consists in decomposing the specification into an invariantand a termination condition.展开更多
The distributed computer system described in this paper is a set of computernodes interconnected in an interconnection network via packet-switching interfaces.The nodes communicate with each other by means of message-...The distributed computer system described in this paper is a set of computernodes interconnected in an interconnection network via packet-switching interfaces.The nodes communicate with each other by means of message-passing protocols. Thispaper presents the implementation of rendezvous facilities as highlevel prhoitives provided by a parallel programming language to support interprocess cornmunication andsynchronisation.展开更多
文摘This paper analyzes some problems of the current teaching situation in the course High-level Programming Language,such as the lagging content of the course compared with technology development,the emphasis on theory rather than on practice,the low enthusiasm of students for learning,and the weak practical ability of students.In response to the needs of enterprises for talents under the background of New Engineering,especially the cultivation of students’adaptability and practical abilities towards future industries to improve students’knowledge and problemsolving abilities to keep up with the modern technology,this paper proposes the ways and methods to reform and explore the teaching content and teaching methods by integrating industry and education,assisting teaching according to industrial demands,and lowering technology barriers of new technology.The practical effect is evaluated through a survey in class and the follow-up questionnaire after class,and the results show that the effect of the practice is effective.
文摘Network processors (NPs) are widely used for programmable and high-performance networks;however, the programs for NPs are less portable, the number of NP program developers is small, and the development cost is high. To solve these problems, this paper proposes an open, high-level, and portable programming language called “Phonepl”, which is independent from vendor-specific proprietary hardware and software but can be translated into an NP program with high performance especially in the memory use. A common NP hardware feature is that a whole packet is stored in DRAM, but the header is cached in SRAM. Phonepl has a hardware-independent abstraction of this feature so that it allows programmers mostly unconscious of this hardware feature. To implement the abstraction, four representations of packet data type that cover all the packet operations (including substring, concatenation, input, and output) are introduced. Phonepl have been implemented on Octeon NPs used in plug-ins for a network-virtualization environment called the VNode Infrastructure, and several packet-handling programs were evaluated. As for the evaluation result, the conversion throughput is close to the wire rate, i.e., 10 Gbps, and no packet loss (by cache miss) occurs when the packet size is 256 bytes or larger.
基金This work was supported by the National Natural Science Foundation of China(Grant Nos.61370100,61321064)Shanghai Knowledge Service Platform Project(ZF1213)+1 种基金Shanghai Municipal Science and Technology Commission Project(14511100400)Defense Industrial Technology Development Program JCKY(2016212B004-2).
文摘The Spatio-Temporal Consistency Language(STeC)is a high-level modeling language that deals natively with spatio-temporal behaviour,i.e.,behaviour relating to certain locations and time.Such restriction by both locations and time is of first importance for some types of real-time systems.CCSL is a formal specification language based on logical clocks.It is used to describe some crucial safety properties for real-time systems,due to its powerful expressiveness of logical and chronometric time constraints.We consider a novel verification framework combining STeC and CCSL,with the advantages of addressing spatio-temporal consistency of system behaviour and easily expressing some crucial time constraints.We propose a theory combining these two languages and a method verifying CCSL properties in STeC models.We adopt UPPAAL as the model checking tool and give a simple example to illustrate how to carry out verification in our framework.
文摘A program construction method based on Gamma language is proposed. The problemto be solved is specified by first-order predicate logic and a semantic verification program isconstructed directly from the specification. Ways for improving efficiency of the program arealso studied. The method differs from the one proposed by Manna and Waldinger, where aprogram is extracted from the proof of the existence of an object meeting the given specification.On the other hand, it also differs from the classical one used for deriving Gamma programsof Banatre and Le Metayer, which consists in decomposing the specification into an invariantand a termination condition.
文摘The distributed computer system described in this paper is a set of computernodes interconnected in an interconnection network via packet-switching interfaces.The nodes communicate with each other by means of message-passing protocols. Thispaper presents the implementation of rendezvous facilities as highlevel prhoitives provided by a parallel programming language to support interprocess cornmunication andsynchronisation.
