1 /*-----------------------------------------------------------------------
2
3 File : cco_scheduling.c
4
5 Author: Stephan Schulz (schulz@eprover.org)
6
7 Contents
8
9 Stuff for scheduling.
10
11 Copyright 2013 by the author.
12 This code is released under the GNU General Public Licence.
13 See the file COPYING in the main CLIB directory for details.
14 Run "eprover -h" for contact information.
15
16 Changes
17
18 <1> New
19
20 -----------------------------------------------------------------------*/
21
22 #include "cco_scheduling.h"
23
24
25
26 /*---------------------------------------------------------------------*/
27 /* Global Variables */
28 /*---------------------------------------------------------------------*/
29
30 ScheduleCell StratSchedule[] =
31 {
32 {"AutoSched0", AUTOSCHED0, "Auto", 0.5066, 0},
33 {"AutoSched1", AUTOSCHED1, "Auto", 0.2466, 0},
34 {"AutoSched2", AUTOSCHED2, "Auto", 0.08 , 0},
35 {"AutoSched3", AUTOSCHED3, "Auto", 0.06 , 0},
36 {"AutoSched4", AUTOSCHED4, "Auto", 0.0433, 0},
37 {"AutoSched5", AUTOSCHED5, "Auto", 0.03 , 0},
38 {"AutoSched6", AUTOSCHED6, "Auto", 0.0166, 0},
39 {"AutoSched7", AUTOSCHED7, "Auto", 0.0166, 0},
40 {NULL , NoOrdering, NULL , 0.0 , 0}
41 };
42
43
44 /*---------------------------------------------------------------------*/
45 /* Forward Declarations */
46 /*---------------------------------------------------------------------*/
47
48
49 /*---------------------------------------------------------------------*/
50 /* Internal Functions */
51 /*---------------------------------------------------------------------*/
52
53
54
55 /*---------------------------------------------------------------------*/
56 /* Exported Functions */
57 /*---------------------------------------------------------------------*/
58
59 /*-----------------------------------------------------------------------
60 //
61 // Function: ScheduleTimesInit()
62 //
63 //
64 //
65 // Global Variables:
66 //
67 // Side Effects :
68 //
69 /----------------------------------------------------------------------*/
70
ScheduleTimesInit(ScheduleCell sched[],double time_used)71 void ScheduleTimesInit(ScheduleCell sched[], double time_used)
72 {
73 int i;
74 rlim_t sum = 0, tmp, limit;
75
76 limit = 0;
77 if(ScheduleTimeLimit)
78 {
79 if(ScheduleTimeLimit>time_used)
80 {
81 limit = ScheduleTimeLimit-time_used;
82 }
83 }
84 else
85 {
86 if(DEFAULT_SCHED_TIME_LIMIT > time_used)
87 {
88 limit = DEFAULT_SCHED_TIME_LIMIT-time_used;
89 }
90 }
91
92 for(i=0; sched[i+1].heu_name; i++)
93 {
94 tmp = sched[i].time_fraction*limit;
95 sched[i].time_absolute = tmp;
96 sum += tmp;
97 }
98 if(ScheduleTimeLimit)
99 {
100 tmp = limit - sum;
101 sched[i].time_absolute = tmp;
102 }
103 else
104 {
105 sched[i].time_absolute = RLIM_INFINITY;
106 }
107 }
108
109
110 /*-----------------------------------------------------------------------
111 //
112 // Function: ExecuteSchedule()
113 //
114 // Execute the hard-coded strategy schedule.
115 //
116 // Global Variables: SilentTimeOut
117 //
118 // Side Effects : Forks, the child runs the proof search, re-sets
119 // time limits, sets heuristic parameters
120 //
121 /----------------------------------------------------------------------*/
122
ExecuteSchedule(ScheduleCell strats[],HeuristicParms_p h_parms,bool print_rusage)123 pid_t ExecuteSchedule(ScheduleCell strats[],
124 HeuristicParms_p h_parms,
125 bool print_rusage)
126 {
127 int raw_status, status = OTHER_ERROR, i;
128 pid_t pid = 0, respid;
129 double run_time = GetTotalCPUTime();
130
131 ScheduleTimesInit(strats, run_time);
132
133 for(i=0; strats[i].heu_name; i++)
134 {
135 h_parms->heuristic_name = strats[i].heu_name;
136 h_parms->ordertype = strats[i].ordering;
137 fprintf(GlobalOut, "# Trying %s for %ld seconds\n",
138 strats[i].heu_name,
139 (long)strats[i].time_absolute);
140 fflush(GlobalOut);
141 pid = fork();
142 if(pid == 0)
143 {
144 /* Child */
145 SilentTimeOut = true;
146 if(strats[i].time_absolute!=RLIM_INFINITY)
147 {
148 SetSoftRlimit(RLIMIT_CPU, strats[i].time_absolute);
149 }
150 return pid;
151 }
152 else
153 {
154 /* Parent */
155 respid = -1;
156 while(respid == -1)
157 {
158 respid = waitpid(pid, &raw_status, 0);
159 }
160 if(WIFEXITED(raw_status))
161 {
162 status = WEXITSTATUS(raw_status);
163 if((status == SATISFIABLE) || (status == PROOF_FOUND))
164 {
165 if(print_rusage)
166 {
167 PrintRusage(GlobalOut);
168 }
169 exit(status);
170 }
171 else
172 {
173 fprintf(GlobalOut, "# No success with %s\n",
174 strats[i].heu_name);
175 }
176 }
177 else
178 {
179 fprintf(GlobalOut, "# Abnormal termination for %s\n",
180 strats[i].heu_name);
181 }
182 }
183 }
184 if(print_rusage)
185 {
186 PrintRusage(GlobalOut);
187 }
188 /* The following is ugly: Because the individual strategies can
189 fail, but the whole schedule can succeed, we cannot let the
190 strategies report failure to dtandard out (that might confuse
191 badly-written meta-tools (and there are such ;-)). Hence, the
192 TSPT status in the failure case is suppressed and needs to be
193 added here. This is ony partially possible - we take the exit
194 status of the last strategy of the schedule. */
195 switch(status)
196 {
197 case PROOF_FOUND:
198 case SATISFIABLE:
199 /* Nothing to do, success reported by the child */
200 break;
201 case OUT_OF_MEMORY:
202 TSTPOUT(stdout, "ResourceOut");
203 break;
204 case SYNTAX_ERROR:
205 /* Should never be possible here */
206 TSTPOUT(stdout, "SyntaxError");
207 break;
208 case USAGE_ERROR:
209 /* Should never be possible here */
210 TSTPOUT(stdout, "UsageError");
211 break;
212 case FILE_ERROR:
213 /* Should never be possible here */
214 TSTPOUT(stdout, "OSError");
215 break;
216 case SYS_ERROR:
217 TSTPOUT(stdout, "OSError");
218 break;
219 case CPU_LIMIT_ERROR:
220 WriteStr(GlobalOutFD, "\n# Failure: Resource limit exceeded (time)\n");
221 TSTPOUTFD(GlobalOutFD, "ResourceOut");
222 Error("CPU time limit exceeded, terminating", CPU_LIMIT_ERROR);
223 break;
224 case RESOURCE_OUT:
225 TSTPOUT(stdout, "ResourceOut");
226 break;
227 case INCOMPLETE_PROOFSTATE:
228 TSTPOUT(GlobalOut, "GaveUp");
229 break;
230 case OTHER_ERROR:
231 TSTPOUT(stdout, "Error");
232 break;
233 case INPUT_SEMANTIC_ERROR:
234 TSTPOUT(stdout, "SemanticError");
235 break;
236 default:
237 break;
238 }
239 exit(status);
240 return pid;
241 }
242
243
244 /*---------------------------------------------------------------------*/
245 /* End of File */
246 /*---------------------------------------------------------------------*/
247
248
249