With recent efforts to build foundational certified software systems, two different approaches have been proposed to certify thread context switching. One is to certify both threads and context switching in a single l...With recent efforts to build foundational certified software systems, two different approaches have been proposed to certify thread context switching. One is to certify both threads and context switching in a single logic system, and the other certifies threads and context switching at different abstraction levels. The former requires heavyweight extensions in the logic system to support first-class code pointers and recursive specifications. Moreover, the specification for context switching is very complex. The latter supports simpler and more natural specifications, but it requires the contexts of threads to be abstracted away completely when threads are certified. As a result, the conventional implementation of context switching used in most systems needs to be revised to make the abstraction work. In this paper, we extend the second approach to certify the conventional implementation, where the clear abstraction for threads is unavailable since both threads and context switching hold pointers of thread contexts. To solve this problem, we allow the program specifications for threads to refer to pointers of thread contexts. Thread contexts are treated as opaque structures, whose contents are unspecified and should never be accessed by the code of threads. Therefore, the advantage of avoiding the direct support of first-class code pointers is still preserved in our method. Besides, our new approach is also more lightweight. Instead of using two different logics to certify threads and context switching, we employ only one program logic with two different specifications for the context switching. One is used to certify the implementation itself, and the more abstract one is used as an interface between threads and context switching at a higher abstraction level. The consistency between the two specifications are enforced by the global program invariant.展开更多
The paper will discuss the process of code-switching and its cognitive pragmatic motivation from the point of relevance.And code-switching is also regarded as a kind of communicative strategy.The process of the produc...The paper will discuss the process of code-switching and its cognitive pragmatic motivation from the point of relevance.And code-switching is also regarded as a kind of communicative strategy.The process of the production of code-switching is also the cooperation and mutual constrain of communicator’s cognitive environment and ability.Cognitive effect can be obtained through communicator’s processing cognitive environment with their cognitive ability.In this process,the cooperation of cognitive ability and cognitive environment gives a guarantee to successful communication with code-switching.展开更多
基金Supported by the National Natural Science Foundation of China under Grant Nos.90718026 and 60928004,ChinaPostdoctoral Science Foundation under Grant No.20080430770Natural Science Foundation of Jiangsu Province,China under Grant No. BK2008181
文摘With recent efforts to build foundational certified software systems, two different approaches have been proposed to certify thread context switching. One is to certify both threads and context switching in a single logic system, and the other certifies threads and context switching at different abstraction levels. The former requires heavyweight extensions in the logic system to support first-class code pointers and recursive specifications. Moreover, the specification for context switching is very complex. The latter supports simpler and more natural specifications, but it requires the contexts of threads to be abstracted away completely when threads are certified. As a result, the conventional implementation of context switching used in most systems needs to be revised to make the abstraction work. In this paper, we extend the second approach to certify the conventional implementation, where the clear abstraction for threads is unavailable since both threads and context switching hold pointers of thread contexts. To solve this problem, we allow the program specifications for threads to refer to pointers of thread contexts. Thread contexts are treated as opaque structures, whose contents are unspecified and should never be accessed by the code of threads. Therefore, the advantage of avoiding the direct support of first-class code pointers is still preserved in our method. Besides, our new approach is also more lightweight. Instead of using two different logics to certify threads and context switching, we employ only one program logic with two different specifications for the context switching. One is used to certify the implementation itself, and the more abstract one is used as an interface between threads and context switching at a higher abstraction level. The consistency between the two specifications are enforced by the global program invariant.
文摘The paper will discuss the process of code-switching and its cognitive pragmatic motivation from the point of relevance.And code-switching is also regarded as a kind of communicative strategy.The process of the production of code-switching is also the cooperation and mutual constrain of communicator’s cognitive environment and ability.Cognitive effect can be obtained through communicator’s processing cognitive environment with their cognitive ability.In this process,the cooperation of cognitive ability and cognitive environment gives a guarantee to successful communication with code-switching.
