1 | % (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | :- module(counter, [ | |
6 | counter_init/0, | |
7 | new_counter/1, | |
8 | get_counter/2, | |
9 | set_counter/2, | |
10 | inc_counter/1, inc_counter/2, | |
11 | inc_counter_by/2, | |
12 | reset_counter/1 | |
13 | ]). | |
14 | ||
15 | :- load_files(library(system), [when(compile_time), imports([environ/2])]). | |
16 | :- (environ(prob_c_counter,X) -> format('environ(prob_c_counter,~w)~n',[X]) ; true). | |
17 | ||
18 | :- if((predicate_property(load_foreign_resource(_), _), \+ environ(prob_c_counter,false))). | |
19 | ||
20 | % C implementation of counter for better performance on SICStus. | |
21 | % A good test is 1748, where this gains maybe 1 second for 22 second model checking time | |
22 | ||
23 | foreign_resource('counter', [new_counter,get_counter,inc_counter,set_counter,reset_counter]). | |
24 | foreign(new_counter, c, new_counter(+atom)). | |
25 | foreign(get_counter, c, get_counter(+atom, [-integer])). | |
26 | foreign(inc_counter, c, inc_counter(+atom, [-integer])). | |
27 | foreign(set_counter, c, set_counter(+atom, +integer)). | |
28 | foreign(reset_counter, c, reset_counter(+atom)). | |
29 | ||
30 | % with this line below we need to adapt the Makefile to include the counter resource in the binary: | |
31 | % (maybe this is a good idea) | |
32 | % :- load_foreign_resource(counter). | |
33 | ||
34 | ||
35 | :- use_module(probsrc(pathes_lib),[safe_load_foreign_resource/2]). | |
36 | ||
37 | :- dynamic loaded/1. | |
38 | ||
39 | counter_init :- | |
40 | (loaded(_) -> true | |
41 | ; assertz(loaded(failure)), | |
42 | %assert_dir, | |
43 | assertz(user:library_directory('.')), | |
44 | (safe_load_foreign_resource(counter,counter) | |
45 | -> retractall(loaded(_)), | |
46 | assertz(loaded(success)) | |
47 | ; format(user_output,"You can set the environment variable prob_c_counter to false to avoid using the counter C++ library~n",[]) | |
48 | ) | |
49 | ). | |
50 | ||
51 | inc_counter_by(Counter,1) :- !, | |
52 | inc_counter(Counter,_). | |
53 | inc_counter_by(Counter,Incr) :- | |
54 | get_counter(Counter,Old), | |
55 | New is Old+Incr, | |
56 | set_counter(Counter,New). | |
57 | ||
58 | %----------------------- | |
59 | :- else. | |
60 | %----------------------- | |
61 | ||
62 | :- write('Using Prolog counter instead of C++ extension'),nl. | |
63 | ||
64 | % Pure Prolog implementation for compatibility. | |
65 | ||
66 | % we now use the SICStus blackboard primitives; they are also available in SWI when using expects_dialect(sicstus4). | |
67 | % we have to ensure there are no clashes with other uses of bb_put, bb_get, ... | |
68 | % currently only memoization.pl uses it in profiling mode | |
69 | ||
70 | % Previously we used assertz/retract | |
71 | % Note: we first set new value before we retract old value to ensure we have no problem if time-out/CTRL-C happens in th emiddle; maybe we can use clause references to make this efficient | |
72 | % blackboard primitives ensure atomic updates out-of-the-box | |
73 | ||
74 | ||
75 | counter_init. | |
76 | ||
77 | get_counter(Counter,Value) :- bb_get(Counter,Value). | |
78 | ||
79 | set_counter(Counter, Value) :- bb_update(Counter,_,Value). | |
80 | ||
81 | new_counter(Counter) :- bb_put(Counter,0). | |
82 | ||
83 | reset_counter(Counter) :- bb_put(Counter,0). | |
84 | ||
85 | inc_counter(Counter, New) :- bb_get(Counter,Old), New is Old+1, bb_update(Counter,_,New). | |
86 | ||
87 | inc_counter_by(Counter, Incr) :- bb_get(Counter,Old), New is Old+Incr, bb_update(Counter,_,New). | |
88 | ||
89 | ||
90 | :- endif. | |
91 | %----------------------- | |
92 | ||
93 | % code for both versions: | |
94 | ||
95 | inc_counter(Counter) :- | |
96 | inc_counter(Counter, _NewVal). | |
97 | ||
98 | ||
99 | % :- statistics(walltime,_),counter:new_counter(bench), repeat, counter:inc_counter(bench,N), N>1000000, statistics(walltime,[_,W]), print(W),nl. | |
100 | % C: 465 - 467 ms, Prolog: 721 - 728 ms, SWI Prolog 1955-1960 ms | |
101 | % C dropped to 259 - 266 ms when dropping checking for inc_counter | |
102 | ||
103 | % :- statistics(walltime,_),bb_put(b,0), repeat, bb_get(b,C),C1 is C+1, bb_update(b,_,C1), C1>1000000, statistics(walltime,[_,W]), print(W),nl. | |
104 | % around 590 ms -> faster than assertz; we should use this for the Prolog counter ! | |
105 | % around 396 in SWI! | |
106 | ||
107 | % statistics(walltime,_),counter:new_counter(b), counter:new_counter(c), repeat,counter:set_counter(c,0), counter:inc_counter(b,N), N>1000000, statistics(walltime,[_,W]), print(W),nl. | |
108 | % C : 451 - 459 ms, Prolog: 1306 - 1342 ms | |
109 | ||
110 | ||
111 | % a good probcli performance test is this one: | |
112 | % probcli ../prob_examples/public_examples/B/PerformanceTests/ModelChecking/Lift_1Million.mch -mc 100000 -disable-time-out |