客服电话
APP下载
迪恩网络APP
随时随地掌握行业动态
官方微信
扫描二维码
关注迪恩网络微信公众号
开源软件名称（OpenSource Name）：Kotlin/kotlinx-lincheck开源软件地址(OpenSource Url)：https://github.com/Kotlin/kotlinx-lincheck开源编程语言(OpenSource Language)：Kotlin 81.6%开源软件介绍(OpenSource Introduction)：kotlinx-lincheck
Lincheck is a framework for testing concurrent data structures for correctness. In order to use the framework, operations to be executed concurrently should be specified with the necessary information for an execution scenario generation. With the help of this specification, lincheck generates different scenarios, executes them in concurrent environment several times and then checks that the execution results are correct (usually, linearizable, but different relaxed contracts can be used as well). The artifacts are available in Bintray and JCenter.
Use Given talks:
This is a fork of Lin-Check framework by Devexperts; the last one is no longer being developed. Table of contents
Test structureThe first thing we need to do is to define operations to be executed concurrently. They are specified as Initial stateIn order to specify the initial state, the empty argument constructor is used. It is guaranteed that before every test invocation a new test class instance is created. Operations and groupsAs described above, each operation is specified via @Operation
public Integer poll() { return q.poll(); }Calling at most onceIf an operation should be called at most once during the test execution, you can set Exception as a resultIf an operation can throw an exception and this is a normal result (e.g. @Operation(handleExceptionsAsResult = NoSuchElementException.class)
public int remove() { return queue.remove(); }Operation groupsIn order to support single producer/consumer patterns and similar ones, each operation could be included in an operation group. Then the operation group could have some restrictions, such as non-parallel execution. In order to specify an operation group,
Here is an example with single-producer multiple-consumer queue test: @OpGroupConfig(name = "producer", nonParallel = true)
public class SPMCQueueTest {
private SPMCQueue<Integer> q = new SPMCQueue<>();
@Operation(group = "producer")
public void offer(Integer x) { q.offer(x); }
@Operation
public Integer poll() { return q.poll(); }
}A generator for Parameter generatorsIf an operation has parameters then generators should be specified for each of them. There are several ways to specify a parameter generator: explicitly on parameter via For setting a generator explicitly, It is also possible to use once configured generators for several parameters. This requires adding this If the parameter generator is not specified lincheck tries to use the default one, binding supported primitive types with the existent generators and using the default configurations for them. Binding parameter and generator namesJava 8 came with the feature (JEP 188) to store parameter names to class files. If test class is compiled this way then they are used as the name of the already specified parameter generators. For example, the two following code blocks are equivalent. @Operation
public Integer get(int key) { return map.get(key); }@Operation
public Integer get(@Param(name = "key") int key) {
return map.get(key);
}Unfortunately, this feature is disabled in javac compiler by default. Use <plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-compiler-plugin</artifactId>
<configuration>
<compilerArgument>-parameters</compilerArgument>
</configuration>
</plugin>However, some IDEs (such as IntelliJ IDEA) do not understand build system configuration as well as possible and running a test from these IDEs will not work. In order to solve this issue you can add Custom scenariosSometimes, it is important to be confident that the testing algorithm works under some corner-case situations.
For this purpose, lincheck provides a possibility to specify custom scenarios via a special Kotlin DSL in a way similar to the example below.
After the scenario is defined, it can be added to the configuration via Custom scenario generation in Kotlin can be done as follows: val scenario = scenario {
initial { // initialize the queue with two elements
actor(SPMCQueue::offer, 1)
actor(SPMCQueue::offer, 2)
}
parallel {
thread { // one producer
// add elements one-by-one
elements.forEach { actor(SPMCQueue::offer, it) }
}
repeat(2) { // two consumers
thread {
repeat(3) { // add three poll-s
actor(SPMCQueue::poll)
}
}
}
}
}
// Add this custom scenario to the test configuration
options.addCustomScenario(scenario)Sequential specificationBy default, lincheck sequentially uses the testing data structure to define the correct specification.
However, it is sometimes better to define it explicitly, by writing a simple sequential implementation, and be sure that it is correct.
Thus, lincheck can test that the testing data structure is correct even without parallelism.
This sequential specification class should have the same methods as the testing data structure.
The specification class can be defined via Validation functionsIt is possible in lincheck to add the validation of the testing data structure invariants, which is implemented via functions that can be executed multiple times during execution when there is no running operation in an intermediate state (e.g., in the stress mode they are invoked after each of the init and post part operations and after the whole parallel part). Thus, these functions should not modify the data structure. Validation functions should be marked with class MyLockFreeListTest {
private val list = MyLockFreeList<Int>()
@Validate
fun checkNoRemovedNodesInTheList() = check(!list.hasRemovedNodes()) {
"The list contains logically removed nodes while all the operations are completed: $list"
}
...
}Parameter and result typesThe standard parameter generators are provided for the basic types like Run testIn order to run a test, @StressCTest // stress execution strategy is used
public class MyConcurrentTest {
<empty constructor and operations>
@Test
public void runTest() {
LinChecker.check(MyConcurrentTest.class);
}
}It is possible to add several Execution strategiesThe section above describes how to specify the operations and the initial state, whereas this section is about executing the test. Using the provided operations lincheck generates several random scenarios and then executes them using the specified execution strategy. At this moment, only stress strategy is implemented, but a model checking one will be added soon. Stress testingThe first implemented in lincheck strategy is stress testing. This strategy uses the same idea as In order to use this strategy, just
Model checkingMost of the complicated concurrent algorithms either use the sequentially consistent memory model under the hood, or bugs in their implementations can be re-produced under it.
Therefore, in lincheck we have a model checking mode that works under the sequentially consistent memory model. Intuitively, it studies all possible schedules with a bounded number of context switches by fully controlling the execution and putting context switches in different locations in threads. Similarly to the stress testing, it is possible to bound the number of schedules (invocations) to be studied -- this way, the test time is predictable independently on the scenario size and the algorithm complexity. To be short, lincheck starts with studying all interleavings with one context switch, but does this evenly, trying to explore different interleavings at first -- this way, we increase the total coverage if the number of available invocations is not enough to study all the interleavings. Once all the interleavings with one context switch are reviewed, it starts examining interleavings with two context switches, and so on, until the available invocations exceed the maximum or all interleavings are covered. This strategy helps not only to increase the testing coverage but also to find an incorrect schedule with the lowest number of context switches possible as well -- this is significant for further bug investigation. Since lincheck controls the execution, it also provides a trace that leads to the found incorrect result. It is worth noting that our model checking implementation is deterministic if the testing data structure is, so that errors are reproducible. Thus, it is recommended not to use Similarly to the stress strategy, model checking can be activated via
Modular testingIt is a common pattern to use linearizable data structures as building blocks of other ones.
At the same time, the number of all possible interleavings for non-trivial algorithms usually is enormous.
This leads us to add a way of modular testing, so that the internal data structures are tested separately, and the operations in them are considered as The atomicity contracts can be specified via Additionally to marking methods as atomic, it is possible to ignore them for the analysis; this is extremely useful for logging and debugging methods. For such methods, Java 9+ supportPlease note that the current version requires the following JVM property
if the testing code uses classes from State representationFor both the stress testing and the model checking strategies, it is possible to enable state reporting. For this purpose, a method that returns Correctness contractsOnce the generated scenario is executed using the specified strategy, it is needed to verify the operation results for correctness. By default lincheck checks the result for linearizability, which is de-facto a standard type of correctness. However, there are also verifiers for some relaxed contracts, which should be set via LinearizabilityLinearizability is a de-facto standard correctness contract for thread-safe algorithms. Roughly, it says that an execution
is correct if there exists an equivalent sequential execution which produces the same results and does not violate
the happens-before ordering of the initial one. By default, lincheck tests data structures for linearizability using Essentially, States equivalencyIn order not to have state duplicates, equivalency relation between test instance states should be defined with Test example@StressCTest(verifier = LinearizabilityVerifier.class)
public class ConcurrentQueueTest extends VerifierState {
private Queue<Integer> q = new ConcurrentLinkedQueue<>();
@Operation
public Integer poll() {
return q.poll();
}
@Operation
public boolean offer(Integer val) {
return q.offer(val);
}
@Override
protected Object extractState() {
return q;
}
}SerializabilitySerializability is one of the base contracts, which ensures that an execution is equivalent to the one that invokes operations in any serial order. The Alike linearizability verification, it also constructs a transition graph
and expects Quiescent consistencyQuiescent consistency is a stronger guarantee than serializability but still relaxed comparing to linearizability. It ensures that an execution is equivalent to some operations sequence which produces the same results and does not reorder operation between quiescent points. Quiescent point is a cut where all operations before the cut are happens-before all operations after it. In order to check for this consistency, use Alike linearizability verification, it also constructs a transition graph
and expects Test example@StressCTest(verifier = QuiescentConsistencyVerifier.class)
public class QuiescentQueueTest extends VerifierState {
private QuiescentQueue<Integer> q = new QuiescentQueue<>();
// Only this operation is quiescent consistent
@Operation
@QuiescentConsistent
public Integer poll() {
return q.poll();
}
@Operation
public boolean offer(Integer val) {
return q.offer(val);
}
@Test
public void test() {
LinChecker.check(QuiescentQueueTest.class);
}
// extractState() here
}Blocking data structuresLincheck supports blocking operations implemented with Most of such blocking algorithms can be formally described via the dual data structures formalism (see the paper below). In this formalism, each blocking operation is divided into two parts: the request (before suspension point) and the follow-up (after resumption); both these parts have their own linearization points, so they may be treated as separate operations within happens-before order. Splitting blocking operations into those parts allows to verify a dual data structure for contracts described above in the way similar to plain data structures. Example with a rendezvous channelFor example, consider a rendezvous channel.
There are two types of processes, producers and consumers, which perform Having the execution results below, where the first thread completes sending 42 to the channel, and the second one receives 42 from it, we have to construct a sequentional execution which produces the same results. By splitting
Similarly, we could split the States equivalencyEquivalency relation among LTS states is defined by equivalency of the following properties:
Lincheck maintains both lists of registered requests and sets of resumed ones internally, while the externally observable state should be defined by the user. The externally observable state is defined in the same way as for plain data structures, with In case of buffered channels,
the externally observable state can be represented with both elements from the buffer and waiting override fun extractState(): Any {
val elements = mutableListOf<Int>()
while (!ch.isEmpty) elements.add(ch.poll()!!)
|
2023-10-27
2022-08-15
2022-08-17
2022-09-23
2022-08-13
六六分期app的软件客服如何联系？不知道吗？加qq群【895510560】即可！标题：六六分期
今天小编告诉大家如何处理win10系统火狐flash插件总是崩溃的问题，可能很多用户都不知
今天小编告诉大家如何对win10系统删除桌面回收站图标进行设置，可能很多用户都不知道
今天小编告诉大家如何对win10系统电脑设置节能降温的设置方法，想必大家都遇到过需要
我们在使用xp系统的过程中,经常需要对xp系统无线网络安装向导设置进行设置，可能很多
今天小编告诉大家如何处理win7系统玩cf老是与主机连接不稳定的问题，可能很多用户都不
电脑对日常生活的重要性小编就不多说了，可是一旦碰到win7系统设置cf烟雾头的问题，很
我们在日常使用电脑的时候，有的小伙伴们可能在打开应用的时候会遇见提示应用程序无法
今天小编告诉大家如何对win7系统打开vcf文件进行设置，可能很多用户都不知道怎么对win
今天小编告诉大家如何对win10系统s4开启USB调试模式进行设置，可能很多用户都不知道怎
请发表评论